Logic
First-order logic is the standard system and language used in mathematics. Logic provides the tools we need to define, as best we can, what a proposition is, what truth is, and how to quantify expressions. Logic, and moreover mathematical logic, are fields of study in their own right far too large to be described fully in this section. Instead, we will be examining the minimum amount of logic needed to provide as a framework on which to build ZFC set theory on top of.
(TO-DO)
Rewrite to be less bad. Talk about lack of definitions for string and stuff. Philosophicle mumbo jumbo.
Introduction
Propositional logic deals with propositions, statements that can be true or false, and relations between propositions. First-order logic is an extension of propositional logic introducing predicates and quantifiers. Predicates allow us to represent a property of an object and quantifiers allow us to reason about the properties of all variables in our domain.
First-order logic can be broken down into two parts. The syntax determines which symbols and formulas we can form, and the semantics determines the meaning of those formulas and how truth can be assigned.
Syntax
We will start with a list of logical symbols, sometimes referred to as the alphabet of first-order logic
Connectives - \land, \lor, \implies, \iff, \lnot
Quantifiers - \forall, \exists
Variables - An infinite set of variables x_1,x_2,x_3,\dots,x_n. Although other letters in the alphabhet, both capital and lowercase may be used.
Punctuation - Right ) and left ( parenthesis, commas, colons, bars \mid, and any other similar symbol.
Equality - The equal sign =.
Our connectives each have special meanings, \land meaning ‘and’, \lor meaning ‘or’, \implies meaning ‘implies’, \iff meaning ‘if and only if’ and \lnot meaning ‘not’. We are also given two quantifiers to work with. \forall meaning ‘for all’ or ‘for every’, and \exists meaning ‘there exists’.
We also have some non-logical symbols called predicates (essentially relations) and functions. These have no meaning by themselves, but serve as a placeholder to be used by theories built on first-order logic. For example, we will soon see ZFC uses a predicate \exists in it’s axioms, so we need an arbitrary predicate in our list of symbols for ZFC to use. To be safe we include an infinite list of predicate and function symbols.
Predicates - An infinite set of predicates P_1,P_2,P_3,\dots,P_n. Although other letters in the alphabhet, both capital and lowercase may be used.
Functions - An infinite set of functions f_1,f_2,f_3,\dots,f_n. Although other letters in the alphabhet, both capital and lowercase may be used.
Predicates and functions may take any number of variables as arguments, which may be notated in the obvious way P(x) for a predicate taking one argument, P(x,y) for two, etc. If the number of arguments is irrelevant however we simply write P.
While ZFC doesn’t use any functions in its axioms and only uses one predicate, some alternate theories built on first-order logic use many.
The syntax covers more than just the symbols used, it also shows us how to construct meaningful formulas from them. If we were to just string these symbols together randomly we could create abominations like
\forall \forall \exists ((\lnot\iff =x \exists)
which are clearly nonsensical. In order to prevent these strings from occurring in our study, we’ll define which strings are valid and call them formulas.
Truth and Connectives
Now we’ll look at the actual meaning behind our connectives. A formula is either true or false. There is