Predicate Logic
Predicate logic is also known as first-order logic
Recall in Propositional Logic, we could only use T and F. In predicate logic, we can use other symbols such as
Predicate logic is an extension of propositional logic.
We want to:
- Refer to values/objects
- Symbolize a claim and its value
- Refer to relations between values
- Capture the meaning of a claim to some or all values
Syntax
Untyped predicate logic consists of the following symbols:
- Alphabet
- Constants (a, b, c, true, false, ...)
- Variables (x, y, ...)
- Function symbols
- Predicate symbols
- Logical connectives (
) - Quantifiers (
) - Functuation
- Brackets
- Terms
- Constants and variables are terms
- Function "return" values are terms
Well-formed formulas of predicate logic are defined as follows:
- Proposition symbols and constants are WFF (atomic formulas)
- The result of a predicate symbol is a WFF (also atomic)
- If
and are WFFs, then each of the following are WFF:
- If
is a WFF and is a variable then is a WFF - If
is a WFF and is a variable then is a WFF
Are the following WFF in predicate logic?
Yes
No
Yes
Yes
No
No
Semantics
See: Logic#Semantics
Unlike semantics in propositional logic, we have to deal with functions, quantifiers, etc. So we want to define a domain that we are dealing with.
This may seem like common sense, but remember:
- For a universally quantified variable, the formula
must be true for all substitutions of the value in the domain, so you have to use a conjunction on all substitutions - For a existentially quantified variable, the formula
must be true for some substitution of the value in the domain, so you have to use a disjunction on all substitutions
Boolean Valuation
If you are ever given a set of formulas and asked to find an interpretation where a certain formula property holds, always start with the simplest formula and work your way to the more complicated ones
Validity
An argument is valid iff for all interpretations where the premises are T, the conclusion is T.
Environments
There is a notation that is more well-known, but cumbersome for stating the meaning of a quantification. Instead of specifying our environments with curly braces like sets, we will just use a caret to denote the value of a domain value
We do not want to sub in the values directly to keep syntax and semantics distinct. That is, [].
Provide an interpretation in which the following formula has the truth value T, and demonstrate that the formula has this. Note
solution
Domain =
| Syntax | Meaning |
|---|---|
Demonstration:
For SE212, you may skip the line labeled with (1) in this particular problem
Find an interpretation in which the following formula is true:
solution
Domain =
| Syntax | Meaning |
|---|---|
UHhhhh
Formula Properties
Very similar to Propositional Logic#Formula Properties
Satisfiability
A predicate logic formula
Tautology
Formula
We write
Contradiction
Formula
Consistency
A collection of closed predicate logic formulas is consistent iff there exists an interpretation in which all the formulas are
Provide an interpretation that shows that the following set of formulas is consistent using the semantics of untyped predicate logic.
solution
Remember to start with the simplest formula:
- We know
must always return false because the universal quantifier in formula 3 needs to hold true - From there, looking at formula 1, we see the left side of the iff is false, so the right side must also be false too. Due to the existential quantifier, we must make sure no value exists where
is true - Formula 2 can be seen with the table afterwards
Domain =
| Syntax | Meaning |
|---|---|
Counterexamples
Show that
solution
Domain =
| Syntax | Meaning |
|---|---|
Premise:
Conclusion:
Typed Predicate Logic
A type is a set of possible values
Person =
Then
Becomes
And hence we cannot make the claim that "a dead tree likes ice cream", since
Since we have types, we don't care about predicates vs functions anymore.
When doing proofs, we don't have to worry about the types. However, make sure you don't substitute the wrong type.
Syntax
Typed predicate logic consists of the following symbols:
- Alphabet (same as untyped, except with colon)
- Constants (a, b, c, true, false, ...)
- Variables (x, y, ...)
- Function symbols
- Predicate symbols
- Logical connectives (
) - Quantifiers (
) - Functuation
- Brackets
- Colon
- Terms
- Constants and variables are terms, and may be followed by a type
- Function "return" values are terms
- Logical connective expressions are terms
- I.e if
and are terms of type bool, then
- I.e if
- A quantifier and variable attached to a term is term of type bool
- Formally, if
is a term of type bool and is a variable of type (and all free occurrences of in are still type ), then and are terms of type bool
- Formally, if
Are the following WFF in typed predicate logic?
Yes No, expects as a param, but got No, expects as its first param, but got No, expects as its second param, but got
is the same as is the same as
We can also write the following short forms:
becomes becomes
Type Inference
Are there types that make the following a WFF? If so, find the most general type.
Write out each variable and function: Find which variables map to which functions (e.g takes the same type as for a parameter). Fill in the blanks.
No, we can't have taking different number of arguments
Note that while we could just make everything one type, this wouldn't be the "most general" type. If we did that, then we would just use untyped predicate logic.
Semantics
Find an interpretation in which:
is
Note:
solution
Domain:
| Syntax | Meaning |
|---|---|