If something really is true, the system is capable of proving it.
- The syntactic operator combining one or more logical expressions into a larger expression.
- Example: Two operators are ∧ and ∨.
- A function with one or more Boolean inputs and a Boolean result. I.e., the meaning of a syntactic operator.
- Example: The meaning of ∧ and ∨, e.g., as described by their truth tables.
- Example: nand (mnemonic: "not and"), written ↑, takes in two Boolean values a and b, and returns true exactly when a ∧ b is not true that is, a ↑ b ≡¬ (a ∧ b).
The interpretation of a formula is a domain, together with a mapping from the formula's relation symbols to specifc relations on the domain.
A statement which can be either true or false.
Example: "Your meal will include hashbrowns."
A variable that can either be true or false, representing whether a certain proposition is true or not. Example: HB
If the system (claims to) prove something is true, it really is true.
A WFF which is true under any truth assignment (any way of assigning truejfalse to the propositions).
Example: A − unsafe ⇒ A − unsafe
Example: a ⇒ a ∨ b
- A variable. Example: a, b, ...
- A constant. Example: WaterWorld location F , Kevin Bacon, or the number 3.
- A function applied to one or more terms.
Example: successor (3)
An assignment of a value true or false to each proposition being used.
Example: For the formula a ⇒ a ∧ b, one possible truth assignment is a = true and b = false. With that truth assignment, the formula is false.
A truth table for an expression has a column for each of its propositional variables. It has a row for each different true/false combination of its propositional variables. It has one more column for the expression itself, showing the truth of the entire expression for that row.
A WFF which is false under any truth assignment.
Example: ¬ (A − unsafe ⇒ A − unsafe)
Example: a ⇒¬a
W well-Formed formula (WFF)
- A constant: true or false. (If you prefer brevity, you can write T or F.)
- A propositional variable.
- Example: a
- A negation ¬φ, where φ is a WFF.
- Example: ¬c
- A conjunction φ ∧ ψ, where φ and ψ are WFFs.
- Example: a ∧¬c
- A disjunction φ ∨ ψ, where φ and ψ are WFFs.
- Example: ¬c ∨ a ∧¬c, or equivalently, (¬c) ∨ (a ∧¬c)
- An implication φ ⇒ ψ, where φ and ψ are WFFs.
- Example: ¬c ∨ a ∧¬c ⇒ b, or equivalently, ((¬c) ∨ (a ∧¬c)) ⇒ b
Well-Formed Formula (WFF) for first-order logic
- A constant: true or false.
- An atomic formula: a relation symbol applied to one or more terms.
- Example: nhbr (x, F )
- A negation of a WFF, ¬φ.
- A conjunction of WFFs, φ ∧ ψ.
- A disjunction of WFFs, φ ∨ ψ.
- An implication of WFFs, φ ⇒ ψ.
- A universal quantifcation of a WFF, ∀x :(φ).
- Example: ∀x : (nhbr (x, F ))
- An existential quantifcation of a WFF, ∃x :(φ).
- Example: ∃x : (nhbr (x, F ))