Predicate Logic

Why do we need a new logic, i.e. Predicate Logic, when we already have Predicate Logic, when we already have Propositional Logic?

Consider the following example:

• Every child likes ice cream. (A)
• Billy is a child. (B)
• Therefore, Billy likes ice cream. (C)

If we try to formalize in Propositional Logic, the best we can do is . However, this is not a valid argument.

Predicate Logic allows us to make use of predicates to capture relationships. You can thus do the following:

• round(Earth)

A predicate is a symbol denoting the meaning of an attribute (property) of a value or the meaning of a relationship between two or more values.

• unary predicate = predicate that takes a single value as an argument
• binary predicate = predicate that takes two values as arguments
• n-ary predicate = predicate that takes arguments

constant = symbol denoting a particular value.

To help us in our proofs, use xg when itβs a Genuine Variable and xu when itβs an Genuine Variable and xu when itβs an Unknown Variable.

How do the semantics and proof theory in Predicate Logic differ from Predicate Logic differ from Propositional Logic?

Substitution We define to be the formula obtained by replacing in every free occurrence of variable with .

Be careful with Variable Capture

Whenever we use , must be free for in . Else this would be a Variable Capture.

Natural Deduction

• forall_i (assume xg, conclude q(xg), and then you can conclude for all x . q(x)) β any variable you want afterwards, xg β Genuine Variable
• forall_e β you can get any
• exists_i β new variable xu β Unknown Variable
• exists_e β (exists x . p(x), for some xu assume p(xu), conclude Q, and you can pull Q out) β N/a

Semantic Tableaux

• Forall_nb β you can choose any legal substitution
• not_forall_nb β use the same variable
• exists_nb β you must choose a new variable
• not_exists_nb β Use the same variable

Examples

Counterexample

For a counter example, use the following format: Notice the capitalization of P in the meaning, as well as the := sign, though I have noticed the prof use without it sometimes.

Semantic Tableaux

predicate gives you truth values