My Logic Notes
- A formal logical system consists of a formal language for encoding arguments and a deductive system. Arguments consist of formulae. Arguments usually start with it a set of formulae consist of premises. Arguments seek to prove a formula, called the conclusion.
- The deductive system uses axioms and rules of inference to derive new formulae from existing formulae.
- Propositional logic is branch of mathematical logic, studying truth-false value propositions, constructed from other propositions.
- Propositional logic "strips away real world context". It is a formal language. Formal languages are made of two things: syntax and semantics. The syntax of propositional logic is made of a set of variables and a set of logical connectives. We may also additional add propositional constants to our language. Valid strings in our language are known as formulae.
- The language of propositional logic can be defined with a context-free grammar; it is a context-free language.
- We shall use the logical connectives: , standing for conjunction, disjunction, negation, implication and bi-implication.
- A truth assignment of a formulae is a mapping between variables and truth/falsity.
- Note that can be rewritten as . This makes intuitive sense, as if , and isn't true, this means can't be true. Also note that can be written as .
- A set of logical connectives are adequate if they can represent all logical connectives. is an example of an adequate set.
- The set is also an adequate set. This is the symbol for NAND (which has an opposite truth table to conjunction).
- The set is also an adequate set. This is the the symbol for NOR (which has an opposite truth table to disjunction).
- The symbols and are the symbols for falsity and truth respectively; these are 0-arity logical connectives (also known as propositional constants). They can also be used to create adequate sets.
- The logical connectives are truth-preserving, this means whenever all parameters to the connectives are , the connectives map to . This means that they cannot alone be an adequate set, as it would be impossible to create Boolean functions which are not truth-preserving by only the composition of these functions.
- Another set is also adequate, which can be proven with the identity for and De Morgan's laws.
- Some other properties have are associativity, commutativity and idempotent. These are properties that does not have.
- Two formulae in propositional logic are equivalent if they have the same value under every truth assignment.
- A literal is a propositional variable or a negation.
- Conjunctive normal form is a conjunction of zero or more disjunctions made of one or more literals e.g. .
- Disjunctive normal form is a disjunction of zero of more conjunctions made of one or more literals e.g. .
- A tautology is a formula that is true in every circumstance e.g. .
- A contradiction is a formula that is true in no circumstances.
- If is a set of formulae, and is a formula, then it is the case that if whenever every formula in holds then holds.
- This is a semantic concept as it relies on the meaning of and , as opposed to a syntactic concept.
- If then is a tautology.
- If $\phi \not\models \psi$ then does not necessarily hold whenever all the formulae in hold, $\not\models \psi$ means that is not a tautology.
- If means that is a contradiction, as there are no circumstances in which holds.
- If , then .
- If is satisfiable there is some truth assignment for which all the formulae in hold.
- Hilbert Calculus is a possible deductive system for propositional logic.
- The rule of inference used is called modus ponens and is that if and , then .
- The three axioms used are:
- In propositional logic, Hilbert calculus can within a finite number of application of the above rules on the premises of an argument, derive all valid statements that are true about them. If then we say the conclusion is derivable from the premises , or is a theorem of . Similarly if $\phi \not\vdash \psi$ then is not a theorem of .
- When talking about propositional logic with Hilbert calculus deriving from , we may use .
- Propositional logic with Hilbert calculus is a sound formal system. A formal system is sound if means , in other words only true statements can be proven.
- Propositional logic with Hilbert calculus is a complete formal system. A formal system is complete if means that in other words all true statements can be proven.
- The axioms in Hilbert calculus are also known as axiom schemata. An axiom schema is a propositional formula whose variables can be substituted by any valid formula and the formula is assumed to hold.
- Here is an example of a Hilbert calculus derivation:
- First-order logic is an extension of propositional logic that includes quantified variables. A first-order language consists of functions and predicates. Predicates may be 0-ary in which case they are analogous to propositional variables. All other variables in first-order logic are quantified variables, referring to the domain of discourse. A first-order language may exist without functions, however without predicates, with an arity greater than 0, the first-order language is essentially a propositional language. Predicates go hand-in-hand with quantification, since the quantified variables must be arguments to predicate to be of use.
- In is important however to note in a first-order language, functions and predicates only exist syntactically and have no meaning. A structure of a first-order language provides the semantic meaning to a first-order language. It contains a non-empty set that is the domain, from which quantified variables emerge. (If the domain were empty, then would be ).
- A structure for a first-order language also provides "interpretations" for the functions and predicates.
- A first-order theory consists of a set of axioms for a first-order language. These axioms are assumed as true. For a structure to be a model of a theory, its interpretation of the functions and predicates must satisfy the axioms.
- The functions and predicates of a first-order language are said to be the signature of the first-order language, bearing in mind that they are merely symbols.
- It is also possible to construct a first-order language with an infinite number of functions and an infinite number of predicates. This means that the first-order language can be used with whatever structure is needed to axiomatise a concept.
Properties of Formal Systems
- As stated before propositional logic is both sound and complete. There is another notion of completeness, however, known as negation completeness. A formal system is negation complete if either or can be derived for all . Propositional logic is not negation complete. This can be shown by using a single propositional variable. There is not enough information, to say whether this one propositional variable, holds or not.
- First-order logic is also sound and complete. Kurt Gödel, an Austrian and later American, logician showed the latter in Gödel's completeness theorem.
- This is not necessarily a problem with first-order logic, as it is possible to restrict the predicates and functions as well as add axioms to ensure everything is derivable. This means that it may be possible, and it is indeed, possible to create first-order languages that are negation complete.
- If it is possible to decide whether a formula in some first-order language is universally valid or not, then the formal system is decidable.
- Propositional logic is decidable, by truth tables, although this is highly inefficient in the worst cases.
- Note that if a first-order language is negation complete, this means that it must be decidable, since all possible proofs can be enumerated over, until either a proof of some proposition or its negation is found.
- However, a first-order language sufficiently powerful to express arithmetic cannot be negation complete. This was shown in Gödel's incompleteness theorem. Of course, it is still possible that there exists a general decision procedure for all first-order languages, however this was shown not to be the case by, Alonzo Church through Lambda Calculus, and Alan Turing through Turing machines.
- It is also the case that since first-order languages are, generally undecidable, if we can show a particular first-order language as undecidable, we can also show it as negation incomplete.
- It is also important to note that even though first-order languages are generally undecidable, there are restricted first-order languages such as monadic first-order logic, that is decidable.
- Here is a proof of the soundness of propositional logic with Hilbert calculus:
Proposition: If , then .
Proof: We shall use induction on the length of the derivation. The base case will be for the first line of the derivation. We shall refer to the propositions on each line of the derivation as .
Base Case: The first line of our derivation, can either arise as an axiom or an assumption. All axioms are tautologies so must be true, so if is an application of an axiom, the . Similarly, if it is an assumption then , so .
Inductive Case: Assume . If is an axiom then, it is a tautology, so . if is an assumption then so . Finally if is an application of the modus ponens inference rule, then there must be some , such that and that and appear in the derivation previously. If appears in the derivation then must be true. Since appears in the derivation, then that must also be true. Because of the truth table for implication, must also be true, so .
must appear in its derivation, if
- Here is a proof of the negation incompleteness of first-order logic able to express a sufficient amount of arithmetic i.e. Gödel's incompleteness theorem:
Proposition: The first-order theory of Peano arithmetic is negation incomplete.
Proof: We shall show this by introduce the notion of Gödel numbering. We shall assign a distinct numeric value to every symbol in our first-order language. Then we shall show that any statement in our first-order language consisting of symbols can be encoded as a natural number, by matching them with the first prime numbers. The product of each prime number raised to the power of the numeric value of its respective symbol, is a unique representation of the string as a natural number. This is because the result can be prime factorised, to get the symbols in their original positions. For instance, the first symbol will the exponent of 2 (as a numeric value), in the prime factorisation of the result. This is what is meant by Gödel numbering, every statement in our first-order language is a natural number; or to put it another way, every proof in our first order language can be expressed a natural number.
Note to represent quantified variables, e.g. and a unary notation can be used to represent different variables. E.g. , , . This can be extended to represent as many quantified variables as needed, with a finite number of symbols.
The proof resets on a single predicate , however note that this predicate is not really a predicate (unless you want to it to be). This is because the predicate is really a short-hand for a very long expression in our first-order language. Optionally, you can say there exists a bi-implication in the form , where is a placeholder for this really long expression, in other words, is not necessary. Either the way the predicate relies on a very important notion: all computable functions can be expressed solely with the Peano axioms (well provided the Church-Turing thesis holds). In any case, the predicate holds if is the Gödel-encoded proof of the Gödel-encoded statement with integer substituted in it. Now, we shall make a new short-hand predicate, , holds when there doesn't exist a proof of the Gödel-encoded statement with substituted in it. Now let be the Gödel number of that predicate. Does hold? If it does hold there isn't a proof of . But if it does hold, there must be a proof of . Contradiction. If it doesn't hold, then that means there is a proof of . But since it doesn't hold, there can't be. Contradiction. Both contradictions are due to the completeness of first-order logic, shown by Gödel previously. In other words there is neither a proof of or . Hence there are some statements, for which neither nor hold in the first-order theory of arithmetic.
- Here is a proof of the undecidability of first-order logic:
Proposition: There is no general procedure to verify whether a set of formulae in first-order logic are universally valid.
Proof: In order to prove the aforementioned proposition, we will show there are propositions for which either or must hold, and there does not exist a general procedure to determine whether or are universally valid. To do this we shall show to how to axiomatise Turing machines, a first-order theory, I shall call . The Turing machine we will axiomatise will be represented by the quintuple . Note that the Turing machine, for convenience will have a semi-infinite tape, however, this is equivalent to Turing machine with a two-way infinite tape. shall have the following functions:
- A 0-ary constant,
- A 1-ary successor functions,
shall have the following predicates:
- which holds when the Turing machine is in state after steps, and scanning the square.
- which holds when the Turing machine has symbol after steps on the square.
- A 2-ary equals predicate
shall have the following basic axioms in addition to the axioms for equality:
- i.e. the successor function is injective
- i.e. 0 does not have a successor
- i.e. all numbers other than 0 have predecessors
shall also have the following axioms for the Turing machine's initial configuration:
- Where are the initial symbols on the Turing machine's tape, . Bearing in mind that is to be written formally as the application to 0, times.
- All other tape symbols are blank:
also needs axioms to represent state transitions in the form, or .
- To represent :
- To represent :
- To represent non-changed tape symbols, for all :
To represent whether the machine halts the following sentence can be used, where represents pairs of for which is undefined:
Clearly, because the halting problem is unsolvable, there cannot be an algorithm to decide whether the above proposition holds for a Turing machine. However, clearly there must exist a truth value to the above proposition. Therefore, first-order logic is undecidable.
- Stanford's online Coursera course on Automata Theory. The course is no longer available, but the video lectures have been put on YouTube.
- New Turing Omnibus by A. K. Dewdney
- The Annotated Turing by Charles Petzold
- Logic by Wilfrid Hodges
- Predicate and Propositional Logic: A Model of Argument by Derek Goldrei
- Representing Turing Machines, available here.