Foundation·F01

The logical framework

Classical first-order logic with equality: the language everything here is written in.

Every article on this wiki is a statement in the formal language built from these symbols, together with variables and parentheses. The connectives and quantifiers are fixed by rules of inference, identity by four axioms, and membership by the ZFC axioms.

Part of the logical framework beneath ZFC (classical first-order logic with equality): taken as given rather than proven, it belongs to the language the set-theoretic axioms are stated in.

Remarks

Definitions must bottom out somewhere. The connectives and quantifiers cannot all be defined without circularity: a truth table for explains "and" using "and". Three things can honestly be done, and this wiki does all three. First, take the meaning of each primitive symbol to be its rules of inference (introduction and elimination), following Gentzen: F02, F03, F05, F06, F09, F10. Second, treat the remaining symbols as abbreviations: negation and the biconditional are defined, not primitive. Third, add the one genuinely classical assumption, excluded middle. Why the rules cannot themselves be replaced by another definition is an old observation (Lewis Carroll's tortoise): a rule of inference is something you use, not a premise you cite, and treating it as a premise only starts a regress. On top of this logic sit the four identity axioms F11 F12 F13 F14, and on top of those the ZFC axioms. Lean shows the same layering: implication and the universal quantifier are the primitive dependent function type, while And, Or, Iff, Exists, Not and False are ordinary definitions.

Wikipedia ↗

Propose an edit3 published revisions