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 $A,B\models C$. 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:

• adult(x) means x is an adult
• 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 $n$ 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 $P[t/x]$ to be the formula obtained by replacing in $P$ every free occurrence of variable $x$ with $t$.

Be careful with Variable Capture

Whenever we use $P[t/z]$, $t$ must be free for $z$ in $P$. 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.

Interpretation
1) Domain = {d1 , d2} 
2) Mapping 
Syntax  | Meaning 
−−−−−−−−−−−−−−−−−−−−−
p ( . ) | P(d1) := T  
		| P(d2) := F

Natural Deduction

$⊢(\forall x,y\cdot p(x,y))⟹(\forall y,x\cdot p(x,y))$

1) assume forall x,y . p(x,y) {
2) for every yg,xg {
	3) p(xg, yg) by forall_e on 2
}
4) forall y,x . p(x,y) by forall_i on 2-3
}
5) (forall x,y . p(x,y)) => (forall y,x . p(x,y)) by imp_i on 1-4

$\forall x\cdot p(x,x)⊢\exists y\cdot p(x,y)$

1)  forall x . p(x,x) premise
2) for every xg {
	3) p(xg, xg) by forall_e on 1
}
4) exists y . p(xg, y) by exists_i on 3
}
5) forall x exists y . p(x,y) by forall_i on 2-4

$\exists x\cdot p(x)⊢\neg (\forall x\cdot \neg p(x))$

1) exists x . p(x) premise
2) disprove forall x . !p(x) {
	3) for some xu assume p(xu) {
		4) !p(xu) by forall_e on 2
		5) false by not_e on 3,4
	}
	6)  false by exists_e on 1,3-5
}
7) !(forall x . !p(x)) by raa on 2-6

$\neg (\exists x\cdot p(x))⊢\forall x\cdot \neg p(x)$

1) !(exists x . p(x)) premise
2) for every xg {
	3) disprove p(xg) {
		4) exists x . p(x) by exists_i on 3
		5) false by not_e on 1,4
	}
	6) !p(xg) by raa on 3-5
}
7) forall x . !p(x) by forall_i on 2-6

Semantic Tableaux

predicate gives you truth values

$\exists x\cdot p(x)⊢\neg (\forall x\cdot \neg p(x))$

1) exists x . p(x)
2) !!(forall x . !p(x))
by not_not_nb on 2
3) forall x . !p(x)
by exists_nb on 1
4) p(a) 
by forall_nb on 3
5) !p(a)
closed on 4,5

$\exists x\cdot \neg p(x)⊢\exists x\cdot p(x)⟹q(x)$

1) exists x . !p(x)
2) !(exists x . p(x) => q(x))
by exists on 1
3) !p(xu)
by not_exists_nb on 2
4) forall x . !(p(x) => q(x))
by forall_nb on 4
5) !(p(xu) => q(xu))
by not_imp_nb on 5
6) p(xu)
7) !q(xu)
closed on 3,6

$\forall x\cdot \exists y\cdot \neg wins(x,y)⊢\neg (\exists x\cdot \forall y\cdot wins(x,y))$

1) forall x . exists y . !wins(x,y) premise
2) disprove exists x . exists y . wins(x,y) {
	3) for some xu assume forall y . wins(xu, y) {
		4) exists y . !wins(xu, y) by forall_e on 1
		5) for some yu assume !wins(xu, yu) {
			6)  wins(xu, yu) by forall_e on 3
			7) false by not_e on 5,6
		}
		8) false by exists_e on 4,5-7
	}
	9) false by exists_e on 2l 3-8
}
10) !(exists x . forall y . wins(x,y)) by raa on 2-9

Concepts

• Genuine Variable
• Unknown Variable