Classical Logic Flashcards
Why do we need a richer logical language than provided by propositional logic? Give an example.
When the universe of discourse concerns a large number of objects, how do we state properties about all of those objects? We need quantification that does not exist in propositional logic.
For example, if you want to say all humans are mortals, then here’s no way to define a variable x such that for all x in the universe of discourse, H(x) -> M(x).
In propositional logic, one would need roughly 6.7 billion conjuncts (assuming there are no humans not on planet earth).
How does one compose FOL in relation to propositional logic?
FOL is propositional logic with some added features.
(1) There are quantifiers– there exists, and for all.
(2) There are predicates– which represent relations between individuals.
(3) There are now terms– variables, functions, and constants.
Constants are particular members of the universe of discourse. Variables can take on any value in the universe of discourse. And functions can be n-ary and map terms to terms. Predicates can also be of arbitrary arity.
How does one define terms in FOL?
Terms in the minimal set consisting of all constants, variables, and function symbols of any arity.
How does one define the set of WFF in FOL?
The set of WFF is the minimal set. Bottom is a member of the minimal set. All predicates of any arity are in the set of WFF. If a predicate P in is WFF, so is its negation. Similarly, if predicates P, Q are in WFF, then so are all of their logical connections. Similarly for quantification of predicates over variables.
What is the priority of quantifiers and connectives in FOL?
In descending order: there exists = for all = negation, and, or, implication
In words, what is a subformula?
A subformula is firstly any formula itself. The depending on the logical connective or quantification involved, then the subformula follow intuitively by removing the connective or quantifier level by level and stating the result formula.
How does mathematical induction differ from structural induction?
Mathematical induction proofs are generally based on the natural numbers. We prove for some base case the claim, and then go on to show that the claim holds for all cases enumerated by the natural numbers.
On the other hand structural induction, starts similarly with a base case that some property holds. But then based on the recursive definition of the structure, it is shown that the property also holds for all minimal ways new elements may be constructed. And therefore, it must holds for all the possible elements that could be constructed.
More formally, state how structural induction works in FOL.
Let A be a be property. Assume A holds for all variables, and constants in the set of terms. Then show that if the property A holds for all terms in the argument of an n-arity function symbol, then the property also holds for the function itself.
Let A be a property. A holds for all the WFF, if one can show.
- A holds for all atoms.
- If for all WFF, if A holds for the WFF it also holds for the negation of the WFF.
- For all the connectives if A holds for its subformulas it also holds for the logical connection of those subformulas.
- For quantification, if A holds for a WFF, then it holds over any quantification of the WFF.
What is a bound variable?
In a FOL formula, a bound variable is a variable that is controlled by a quantifier.
What is a free variable?
This is a variable that has no quantifier controlling its occurrence.
What is the scope of a quantifier?
This is the propositional formula over which the quantifier acts.
How can one inductively define the free variables for terms?
- Constants do not constitute free variables. So if c is a constant FV(c) = empty.
- If x is simply a variable, then FV(x) = {x},
- If f is an n-ary function symbol f(t1,t2,…,tn). Then FV(f(t1,t2,…,tn) = FV(t1)UFV(tn)U…UFV(tn).
How can one inductively define the free variables for WFF?
This is fairly intuitive. FV(falsum) = empty. The FV of a predicate are the union of the free variables of its terms. The FV a negated proposition are the same as the FV of the proposition. For the other logical connectives, we take the union of the FV of the subformulae. And for quantified WFF, one removes each variable which is quantifiers from the set of FV of the un-quantified propositional formulae.
How is the substitution operation defined for variables, constants, and functions?
For constants, no substitution occurs. So c[t/x] = c where c is a constant.
For variable y, y[t/x]. This is equation to just y again if y is not equal to x. On the other hand, if y is x, then we substitute and it’s equal to t.
For functions, we simply substitute for each term appearing in the function.
f(t1,…,tn)[t/x] = f(t1[y/x], …, tn[t/x]).
How does substitution work for WFF in FOL?
The case for the logical connectives is intuitive. Simply append the substitution to each subformulae. The case for quantified formula is more intricate.
There are a couple of issues. Consider the substitution [t/x]. If x is quantified over, this substitution creates a problem, so, in fact, we never make such substitutions when x is quantified over.
Another issue is if we quantify over a free variable in the term t, then this creates an issue because it changes the meaning of the term t. In this case, we just generate a new unused propositional variable z that does not appear in the formula P1 or the term t. Now we quantify over this new variable z, instead of the old conflict FV(t). We replace all instances of the old conflicting variable with z. And then we can substitute in [t/x].
Finally, if x is not quantified over, and any quantified variables do not appear in FV(t) then we may make a straightforward substitution of t for x in the formula.
