Notes on Lean, automated theorem proving, etc

- Lean is based on the Calculus of Inductive Constructions
- Coq is based on the Calculus of Constructions, so, similar
- HOL4, HOL Light, Isabelle/HOL: based on simple type theory (Higher-Order Logic)
	- 'Zero-th order logic': propositional logic (P, Q, ... are propositions, and we have implication, negation, etc, and inference rules MP etc)
	- First-order logic: predicate logic (predicates P, Q, ..., quantifiers \forall and \exists, )
	- Second-order logic: extends quantification over predicates, e.g. SOL can express 'the set of all cubes and all tetrahedra', i.e. \exists P, \forall x, P x <-> (Cube(x) or Tetrahedron(x))
		- This \exists P is not allowed in first-order logic; we can only quantify over propositions
	- Higher-order (simple predicate) logic: extends quantification to be arbitrarily nested
- Logics usually have (one or more) syntaxes and semantices
	- The syntax defines the 'language' of the logic; what expressions are valid?
	- For instance, propositional logic (usually) has the following syntax (note, this syntax is ambiguous without precedence/associativity):
		- Term = Var | Term BOp Term | UOp Term | (Term)
		- Var = P | Q | ...
		- BOp = Or | And | Implies | Iff
		- UOp = Not
	- A sentence like "P Implies (Q And R)" is syntactically valid, but does not yet have a meaning without a semantics
	- Semantics defines "what does this sentence mean"
		- Typically defined w.r.t. a model, in the case of propositional logic this is usually a truth valuation
		- Sentences are either true or false, given a model v : Var -> {0, 1}. For instance, given v(x) = 1 if x = p else 0, v |/= p -> q. (p -> q is not true under v, v does not satisfy p -> q)
		- Uses rules such as p -> q is true if p is false or q is true
	- Something something Deductive systems (axioms, inference rules, purely syntactic proofs) 

id: a024d5454e3c49a5afbd4cd4ada5c02b
parent_id: d2eec4f85f0c43a5b8010b14ae41abf9
created_time: 2022-11-01T23:14:34.129Z
updated_time: 2022-11-02T00:44:32.176Z
is_conflict: 0
latitude: 52.37021570
longitude: 4.89516790
altitude: 0.0000
author: 
source_url: 
is_todo: 1
todo_due: 0
todo_completed: 0
source: joplin-desktop
source_application: net.cozic.joplin-desktop
application_data: 
order: 0
user_created_time: 2022-11-01T23:14:34.129Z
user_updated_time: 2022-11-02T00:44:32.176Z
encryption_cipher_text: 
encryption_applied: 0
markup_language: 1
is_shared: 0
share_id: 
conflict_original_id: 
master_key_id: 
type_: 1