Hilbert System for First-Order Logic LOGIC FOR COMPSCI

What are the key differences between propositional and first-order logic regarding their expressive power?

Propositional logic deals with truth values of entire propositions and their combinations using logical connectives. First-order logic extends this by allowing reasoning about objects, their properties (using predicates), relationships between them (also using predicates), and quantification over these objects.

Explain the purpose of an interpretation in first-order logic and what components constitute an interpretation

An interpretation in FOL provides a semantic meaning to the syntactic elements of the logic. It consists of a non-empty domain of objects, assignments of relations to predicate symbols, and assignments of domain elements to constant symbols.

What is the significance of distinguishing between free and bound variables in a first-order logic formula?

The distinction between free and bound variables is crucial for determining a formula's meaning and truth value, especially in the presence of quantifiers. An assignment determines a free variable's value, while the quantifier that binds it determines a bound variable's value

State Axiom 4 of the Hilbert system $\mathcal{L}$ for first-order logic and briefly explain its intuitive meaning

Axiom 4 states $(\forall x A(x) \rightarrow A(a))$, meaning that if a property $A$ holds for all $x$ in the domain, then it must also hold for any specific individual $a$ in that domain. This axiom formalizes the idea of universal instantiation or specialization.

What is the role of the Generalization rule of inference in the Hilbert system $\mathcal{L}$, and what crucial condition must be met when applying it?

The Generalization rule allows us to infer $\forall x A(x)$ from $A(a)$, suggesting that if $A$ holds for an arbitrary individual $a$ (that has not been mentioned in any assumptions), then $A$ must hold for all individuals $x$ in the domain. The condition that $a$ does not appear in any assumption is essential to maintain soundness and avoid incorrect generalizations.

Explain the Deduction Theorem in the context of the Hilbert system $\mathcal{L}$ and why it is a valuable tool for proving theorems.

The Deduction Theorem states that proving $B$ under the assumption of $A$ (from a set of premises $U$) is equivalent to proving the implication $A \rightarrow B$ (from $U$ alone). This theorem simplifies proofs by allowing us to temporarily introduce assumptions and then discharge them by forming implications

Describe the concept of logical equivalence between two first-order logic formulas and provide an example using quantifiers.

Two first-order logic formulas are logically equivalent if they have the same truth value under every possible interpretation. For example, $\forall x \neg P(x) \equiv \neg \exists x P(x)$.

What does it mean for a first-order logic formula to be valid? Give an example of a valid formula.

A first-order logic formula is valid if it is true in every possible interpretation. An example of a valid formula is $\forall x P(x) \rightarrow P(y)$.

Explain how an interpretation can be used to show that a first-order logic formula is invalid.

To show that a formula is invalid, one can construct an interpretation (by specifying a domain and the meaning of the predicates and constants involved) in which the formula evaluates to false. This demonstrates at least one scenario where the formula does not hold

Briefly describe the main idea behind Hilbert-style proofs and their reliance on axioms and inference rules.

Hilbert-style proofs are formal derivations of logical truths (theorems) starting from a fixed set of axioms and applying a small number of inference rules, such as Modus Ponens and Generalization. The goal is to derive all logical truths of the system through these purely syntactic manipulations

Atomic Formula

A basic formula in first-order logic consisting of a predicate symbol applied to a tuple of terms (variables or constants)

Bound Variable

An occurrence of a variable within the scope of a quantifier (either universal or existential) that uses the same variable

Closed Formula (Sentence)

A formula in first-order logic that contains no free variables. Its truth value is independent of any variable assignment.

Constant

A symbol in first-order logic that represents a specific, fixed object in the domain of an interpretation

Domain (of Interpretation)

A non-empty set of objects over which the quantifiers range and to which the terms refer in a given interpretation

Free Variable

An occurrence of a variable in a first-order logic formula not bound by any quantifier. A variable assignment determines its value

Generalization (Rule of Interference)

A rule in the Hilbert system that allows inferring $\forall x A(x)$ from $\vdash A(a)$, provided that the constant $a$ does not appear in any undischarged assumptions.

Hilbert System (for First-Order Logic)

A formal deductive system for first-order logic defined by a specific set of axioms and inference rules (Modus Ponens and Generalization).

Interpretation

In first-order logic, a structure that assigns meanings to the non-logical symbols of the language is a domain of discourse, relations corresponding to predicate symbols, and elements of the domain corresponding to constant symbols.

Logical Consequence

A formula $A$ is a logical consequence of a set of formulas $U$ if every interpretation that makes all formulas in $U$ true also makes $A$ true

Logical Equivalence

Two formulas $A$ and $B$ are logically equivalent if they have the same truth value in every interpretation

Model

An interpretation in which a given formula (or a set of formulas) is true

Modus Ponens (MP)

A fundamental rule of inference that states if $A$ is true and $A \rightarrow B$ is true, then $B$ must also be true.

Predicate

A symbol in first-order logic representing a property of or a relation between objects in the domain

Quantifier (Universal For All and Existential)

Symbols used to express that a property holds for all objects in the domain ($\forall$) or at least one object in the domain ($\exists$)

Satisfiability

A formula is satisfactory if at least one true interpretation exists

Soundness

A deductive system is sound if every formula that can be proven in the system is also logically valid (true in all interpretations)

Specialization (Axiom 4)

The axiom $(\forall x A(x) \rightarrow A(a))$ in the Hilbert system, which expresses that if $A$ holds for all $x$, it holds for any specific $a$.

Term

A linguistic expression in first-order logic that refers to an object in the domain. Terms can be variables or constants

Validity

A formula is valid if it is true in every possible interpretation.

Variable

A symbol in first-order logic that can range over the objects in the domain of an interpretation

Deduction Theorem

A meta theorem stating that $U \cup {A} \vdash B$ if and only if $U \vdash A \rightarrow B$, which links provability of an implication to provability under an assumption.