Bound Variable
A variable that is within the scope of a quantifier (∀,∃) or binding operator, where its value is controlled by that operator. Denoted like: ∀x(P(x)) or ∃x(Q(x)), where x is bound
Unbound Variable
A variable that appears in a formula without being controlled by any quantifier or binding operator. Also called a free variable. In P(x,y), both x and y are unbound if no quantifiers are present
Proposition
A declarative statement that is either true or false, but not both. Also called a propositional variable or atomic formula in formal logic.
Predicate
A statement containing variables that becomes a proposition (true/false) when those variables are given specific values. Denoted as P(x), Q(x,y), etc., where P, Q are predicates and x, y are variables in their domains.
Quantifier
A logical operator that specifies the quantity of specimens in a domain for which a predicate holds. Two main types: universal quantifier ($\forall$: 'for all') and existential quantifier ($\exists$: 'there exists')
Inference
A logical process of deriving a conclusion from given premises through valid logical rules. Symbolically: If P₁, P₂, ..., Pₙ are premises and C is conclusion, write: P₁, P₂, ..., Pₙ ⊢ C
Axiom
A statement accepted as true without proof in a logical system.
Theorem
A statement that has been proven based on axioms and logical rules.
Proof
A logical argument that demonstrates the truth of a statement (conclusion) from given or previously established statements (premises, axioms) through valid rules of inference. Written as: Given P₁,...,Pₙ, prove C
Premise
A proposition or statement (P₁, P₂, ..., Pₙ) assumed or proven to be true, from which a conclusion is drawn. In formal logic notation, premises are listed above a horizontal line with conclusion below: $\frac{P_1,P_2,...,P_n}{C}$
Conclusion
The statement C derived from premises P₁, P₂, ..., Pₙ through valid logical inference. In formal notation: P₁, P₂, ..., Pₙ ⊢ C or $\frac{P_1,P_2,...,P_n}{C}$
Validity
An argument is valid if and only if it is impossible for all premises to be true and the conclusion false. In formal notation: if premises P₁, P₂, ..., Pₙ are true, then conclusion C must be true: (P₁ ∧ P₂ ∧ ... ∧ Pₙ) → C
Soundness
The property of an argument being both valid and having true premises.
Argument
A logical structure consisting of premises P₁, P₂, ..., Pₙ and a conclusion C where the premises are meant to support the conclusion. In formal notation: P₁, P₂, ..., Pₙ ⊢ C or $\frac{P_1,P_2,...,P_n}{C}$
Fallacy
A flaw or error in reasoning that renders an argument invalid.
Contradiction
A statement that is always false regardless of the truth values of its components.
Tautology
A compound proposition that evaluates to true for all possible truth values of its variables. In formal notation: if T is tautology, then T ≡ 1 or ⊨ T
Modus Ponens
A fundamental rule of inference: given (P → Q) and P, we can deduce Q. Formally written as: $\frac{P \to Q,\; P}{Q}$ or (P → Q) ∧ P ⊢ Q
Modus Tollens
A rule of inference: given (P → Q) and ¬Q, we can deduce ¬P. Formally written as: $\frac{P \to Q,\; \neg Q}{\neg P}$ or (P → Q) ∧ ¬Q ⊢ ¬P
Disjunctive Syllogism
A rule of inference: given (P ∨ Q) and ¬P, we can deduce Q. Formally written as: $\frac{P \lor Q,\; \neg P}{Q}$ or (P ∨ Q) ∧ ¬P ⊢ Q
Conjunction
A logical operation combining two statements P and Q with AND (∧), true only when both statements are true. Formally: P ∧ Q is true iff both P and Q are true
Disjunction
A logical operation combining two statements P and Q with OR (∨), true when at least one statement is true. Formally: P ∨ Q is true iff either P is true or Q is true (or both)
Disjunctive Normal Form (DNF)
A logical formula is in DNF if it is a disjunction (OR) of conjunctions (AND) of literals (variables or their negations): $(p \land q) \lor (\neg p \land r) \lor (q \land r)$
Conjunctive Normal Form (CNF)
A logical formula is in CNF if it is a conjunction (AND) of disjunctions (OR) of literals (variables or their negations): $(p \lor q) \land (\neg p \lor r) \land (q \lor r)$
Conditional
A logical operation denoted as P → Q (if P, then Q), establishing a relationship where P implies Q. Formally written as: if P is true and P → Q is true, then Q must be true
Antecedent
In a conditional statement P → Q, the antecedent P is the hypothesis or condition that implies the consequent
Consequent
In a conditional statement P → Q, the consequent Q is the conclusion or result that follows from the antecedent
Biconditional
A logical operation denoted as P ↔ Q (P if and only if Q), indicating that P and Q have the same truth value. Formally: (P → Q) ∧ (Q → P)
Deduction
A form of logical inference where a conclusion necessarily follows from a set of premises. If all premises are true, the conclusion must be true.
Induction
A method of reasoning that derives general principles from specific observations, establishing probable (not certain) conclusions.
Universal Quantifier
Denoted by ∀x P(x), asserts that predicate P holds for every element x in the domain of discourse. Read as 'for all x, P(x)'
Existential Quantifier
Denoted by ∃x P(x), asserts that predicate P holds for at least one element x in the domain of discourse. Read as 'there exists x such that P(x)'
Logical Connective
Operators that combine simple propositions into compound propositions, forming the basic building blocks of logical expressions
Implication
A logical relationship P → Q between statements P (antecedent) and Q (consequent) where P implies Q. The implication is false only when P is true and Q is false.
Equivalence
Two logical statements $p$ and $q$ are equivalent ($p \equiv q$) if they have identical truth values under all possible valuations of their variables
Negation
A unary logical operator (¬P or ~P) that reverses the truth value of a proposition P. If P is true, ¬P is false; if P is false, ¬P is true.
Satisfiability
A logical formula is satisfiable if there exists at least one assignment of truth values to its variables that makes the entire formula true. Formally: ∃x₁...∃xₙ φ(x₁,...,xₙ) = true
Logical Form
The underlying structure of a logical statement abstracted from its specific content, revealing the logical relationships between its components.
Logical Consistency
A set of statements is logically consistent if and only if there exists at least one interpretation under which all statements in the set are true simultaneously. Formally: ∃M(M ⊨ φ₁ ∧ φ₂ ∧ ... ∧ φₙ)
Rule of Inference
A pattern of reasoning Γ ⊢ φ that preserves truth, where Γ is a set of premises and φ is the conclusion
Logical Consequence
A statement φ is a logical consequence of premises Γ (written Γ ⊨ φ) if φ is true in every model where all premises in Γ are true
Formal System
A mathematical structure consisting of a formal language L, a set of axioms A, and a set of inference rules R that together define valid derivations. Denoted as FS = (L, A, R)
Formal Language
A set of strings over an alphabet Σ, defined by precise formation rules. L ⊆ Σ*
Natural Deduction
A proof system that models logical reasoning through introduction and elimination rules for logical connectives. Proofs are trees of judgments Γ ⊢ φ
Sequent Calculus
A formal proof system using sequents of the form Γ ⊢ Δ, where Γ and Δ are finite multisets of formulas. Read as 'Γ entails Δ'
Truth Table
A systematic listing of all possible combinations of truth values for atomic propositions and the resulting truth values of compound expressions
Symbolic Representation
A formal system of notation using well-defined symbols to express logical relationships and operations with precision and clarity
Non-contradiction
The logical principle that asserts ¬(P ∧ ¬P) is always true. No statement can be both true and false in the same sense at the same time
Law of Excluded Middle
The principle that every proposition P is either true or false, formally expressed as P ∨ ¬P
Necessary and Sufficient Conditions
P is necessary for Q if Q → P, and P is sufficient for Q if P → Q. If both hold, then P ↔ Q
Propositional Calculus
A formal system dealing with propositions and logical connectives, where formulas are built from atomic propositions using logical operators
First-order Logic
A formal system extending propositional logic with quantifiers (∀, ∃) and predicates, allowing expression of relationships and properties
Higher-order Logic
A logical system allowing quantification over predicates, functions, and other higher-order objects, extending first-order logic's expressiveness
Interpretation
A mapping I from a formal language L to a domain D that assigns semantic meaning to the symbols and expressions of L. Written as I: L → D
Model Theory
Mathematical study of the relationship between formal theories T and their models M, where M ⊨ T denotes M is a model of T
Proof Theory
Study of formal proofs as mathematical objects and the structural relationships between them
String
A finite sequence s = a₁a₂...aₙ where each aᵢ belongs to an alphabet Σ. Formally written as s ∈ Σ*
Expression
A syntactically valid combination of symbols according to formation rules of a formal system
Elementary Proposition
An atomic statement P that has a truth value and cannot be decomposed into simpler logical statements
Syntax Tree
A hierarchical data structure T = (V,E,r) representing the grammatical structure of an expression, where V is the set of nodes, E the edges, and r the root
Node
A fundamental unit v ∈ V in a tree structure containing data and maintaining relationships with other nodes through edges E
Leaf Node
A terminal node l ∈ V in a tree structure with no children, formally: l ∈ V such that ∄v ∈ V: (l,v) ∈ E
Root Node
The unique node r ∈ V in a tree structure with no parent, serving as the origin point. Formally: r ∈ V such that ∄v ∈ V: (v,r) ∈ E
Branch
A directed edge e = (u,v) ∈ E in a tree structure connecting a parent node u to a child node v
Partial Proposition
An incomplete logical statement φ(x₁,...,xₙ) containing free variables or undefined terms that requires additional context to determine truth value
Complete Proposition
A logical statement p that is fully specified and has a well-defined truth value under any given interpretation I
Degree of Syntax Tree
The maximum number d of child nodes for any node v in the tree T. Formally: d = max{|children(v)| : v ∈ V}
Construction Sequence
An ordered sequence of steps S = (s₁, s₂, ..., sₙ) that, when executed in order, produces a valid logical structure or proof
Compound Proposition
A proposition p constructed by combining simpler propositions using logical connectives. Formally: p := q ∘ r where ∘ ∈ {∧, ∨, →, ↔}
Substitution
An operation σ that replaces variables or subexpressions with other expressions. Formally: σ: V → Terms where V is the set of variables
Structural Induction
A proof technique establishing that a property P holds for all instances of a recursively defined structure S by showing it holds for base cases and is preserved by construction steps
Absorption
A logical law stating that $P \land (P \lor Q) \equiv P$ and $P \lor (P \land Q) \equiv P$. Also known as the absorption laws in Boolean algebra.
Assignment, Valuation
A function $v: Vars \to D$ that assigns values from domain $D$ to variables in a logical expression, or more generally, an interpretation that maps symbols to their semantic values.
Bijection
A function $f: A \to B$ that is both injective (one-to-one) and surjective (onto). For every element $b \in B$, there exists exactly one element $a \in A$ such that $f(a) = b$.
Calculus
A formal system or method of reasoning in logic and mathematics. In logic, refers to various symbolic calculation systems like propositional calculus, predicate calculus, or lambda calculus.
Cardinality
The measure of the size of a set, denoted $|A|$ or $card(A)$. For finite sets, it's the number of elements. For infinite sets, it distinguishes different sizes of infinity.
Class
In set theory and logic, a collection of objects or elements that may be too large to form a set. Used to handle collections that would lead to paradoxes if considered as sets (like the class of all sets).
Clause
In logic, a disjunction of literals (atomic formulas or their negations). In propositional logic, a clause has the form $L_1 \lor L_2 \lor ... \lor L_n$ where each $L_i$ is a literal.
Closed formula (Sentence)
A formula with no free variables. All variables are bound by quantifiers or other binding operators. A sentence can be evaluated to true or false without additional context.
Closed term (Ground term)
A term containing no variables, only constants and function symbols. Ground terms represent specific objects in the domain without any unspecified parameters.
Compactness
A fundamental property of first-order logic stating that if every finite subset of a set of sentences Γ has a model, then the entire set Γ has a model. Formally: if Γ ⊨ φ, then there exists finite Γ₀ ⊆ Γ such that Γ₀ ⊨ φ.
Bound Variable
A variable that is within the scope of a quantifier (∀,∃) or binding operator, where its value is controlled by that operator. Denoted like: ∀x(P(x)) or ∃x(Q(x)), where x is bound
Unbound Variable
A variable that appears in a formula without being controlled by any quantifier or binding operator. Also called a free variable. In P(x,y), both x and y are unbound if no quantifiers are present
Proposition
A declarative statement that is either true or false, but not both. Also called a propositional variable or atomic formula in formal logic.
Predicate
A statement containing variables that becomes a proposition (true/false) when those variables are given specific values. Denoted as P(x), Q(x,y), etc., where P, Q are predicates and x, y are variables in their domains.
Quantifier
A logical operator that specifies the quantity of specimens in a domain for which a predicate holds. Two main types: universal quantifier ($\forall$: 'for all') and existential quantifier ($\exists$: 'there exists')
Inference
A logical process of deriving a conclusion from given premises through valid logical rules. Symbolically: If P₁, P₂, ..., Pₙ are premises and C is conclusion, write: P₁, P₂, ..., Pₙ ⊢ C
Axiom
A statement accepted as true without proof in a logical system.
Theorem
A statement that has been proven based on axioms and logical rules.
Proof
A logical argument that demonstrates the truth of a statement (conclusion) from given or previously established statements (premises, axioms) through valid rules of inference. Written as: Given P₁,...,Pₙ, prove C
Premise
A proposition or statement (P₁, P₂, ..., Pₙ) assumed or proven to be true, from which a conclusion is drawn. In formal logic notation, premises are listed above a horizontal line with conclusion below: $\frac{P_1,P_2,...,P_n}{C}$
Conclusion
The statement C derived from premises P₁, P₂, ..., Pₙ through valid logical inference. In formal notation: P₁, P₂, ..., Pₙ ⊢ C or $\frac{P_1,P_2,...,P_n}{C}$
Validity
An argument is valid if and only if it is impossible for all premises to be true and the conclusion false. In formal notation: if premises P₁, P₂, ..., Pₙ are true, then conclusion C must be true: (P₁ ∧ P₂ ∧ ... ∧ Pₙ) → C
Soundness
The property of an argument being both valid and having true premises.
Argument
A logical structure consisting of premises P₁, P₂, ..., Pₙ and a conclusion C where the premises are meant to support the conclusion. In formal notation: P₁, P₂, ..., Pₙ ⊢ C or $\frac{P_1,P_2,...,P_n}{C}$
Fallacy
A flaw or error in reasoning that renders an argument invalid.
Contradiction
A statement that is always false regardless of the truth values of its components.
Tautology
A compound proposition that evaluates to true for all possible truth values of its variables. In formal notation: if T is tautology, then T ≡ 1 or ⊨ T
Modus Ponens
A fundamental rule of inference: given (P → Q) and P, we can deduce Q. Formally written as: $\frac{P \to Q,\; P}{Q}$ or (P → Q) ∧ P ⊢ Q
Modus Tollens
A rule of inference: given (P → Q) and ¬Q, we can deduce ¬P. Formally written as: $\frac{P \to Q,\; \neg Q}{\neg P}$ or (P → Q) ∧ ¬Q ⊢ ¬P
Disjunctive Syllogism
A rule of inference: given (P ∨ Q) and ¬P, we can deduce Q. Formally written as: $\frac{P \lor Q,\; \neg P}{Q}$ or (P ∨ Q) ∧ ¬P ⊢ Q
Conjunction
A logical operation combining two statements P and Q with AND (∧), true only when both statements are true. Formally: P ∧ Q is true iff both P and Q are true
Disjunction
A logical operation combining two statements P and Q with OR (∨), true when at least one statement is true. Formally: P ∨ Q is true iff either P is true or Q is true (or both)
Disjunctive Normal Form (DNF)
A logical formula is in DNF if it is a disjunction (OR) of conjunctions (AND) of literals (variables or their negations): $(p \land q) \lor (\neg p \land r) \lor (q \land r)$
Conjunctive Normal Form (CNF)
A logical formula is in CNF if it is a conjunction (AND) of disjunctions (OR) of literals (variables or their negations): $(p \lor q) \land (\neg p \lor r) \land (q \lor r)$
Conditional
A logical operation denoted as P → Q (if P, then Q), establishing a relationship where P implies Q. Formally written as: if P is true and P → Q is true, then Q must be true
Antecedent
In a conditional statement P → Q, the antecedent P is the hypothesis or condition that implies the consequent
Consequent
In a conditional statement P → Q, the consequent Q is the conclusion or result that follows from the antecedent
Biconditional
A logical operation denoted as P ↔ Q (P if and only if Q), indicating that P and Q have the same truth value. Formally: (P → Q) ∧ (Q → P)
Deduction
A form of logical inference where a conclusion necessarily follows from a set of premises. If all premises are true, the conclusion must be true.
Induction
A method of reasoning that derives general principles from specific observations, establishing probable (not certain) conclusions.
Universal Quantifier
Denoted by ∀x P(x), asserts that predicate P holds for every element x in the domain of discourse. Read as 'for all x, P(x)'
Existential Quantifier
Denoted by ∃x P(x), asserts that predicate P holds for at least one element x in the domain of discourse. Read as 'there exists x such that P(x)'
Logical Connective
Operators that combine simple propositions into compound propositions, forming the basic building blocks of logical expressions
Implication
A logical relationship P → Q between statements P (antecedent) and Q (consequent) where P implies Q. The implication is false only when P is true and Q is false.
Equivalence
Two logical statements $p$ and $q$ are equivalent ($p \equiv q$) if they have identical truth values under all possible valuations of their variables
Negation
A unary logical operator (¬P or ~P) that reverses the truth value of a proposition P. If P is true, ¬P is false; if P is false, ¬P is true.
Satisfiability
A logical formula is satisfiable if there exists at least one assignment of truth values to its variables that makes the entire formula true. Formally: ∃x₁...∃xₙ φ(x₁,...,xₙ) = true
Logical Form
The underlying structure of a logical statement abstracted from its specific content, revealing the logical relationships between its components.
Logical Consistency
A set of statements is logically consistent if and only if there exists at least one interpretation under which all statements in the set are true simultaneously. Formally: ∃M(M ⊨ φ₁ ∧ φ₂ ∧ ... ∧ φₙ)
Rule of Inference
A pattern of reasoning Γ ⊢ φ that preserves truth, where Γ is a set of premises and φ is the conclusion
Logical Consequence
A statement φ is a logical consequence of premises Γ (written Γ ⊨ φ) if φ is true in every model where all premises in Γ are true
Formal System
A mathematical structure consisting of a formal language L, a set of axioms A, and a set of inference rules R that together define valid derivations. Denoted as FS = (L, A, R)
Formal Language
A set of strings over an alphabet Σ, defined by precise formation rules. L ⊆ Σ*
Natural Deduction
A proof system that models logical reasoning through introduction and elimination rules for logical connectives. Proofs are trees of judgments Γ ⊢ φ
Sequent Calculus
A formal proof system using sequents of the form Γ ⊢ Δ, where Γ and Δ are finite multisets of formulas. Read as 'Γ entails Δ'
Truth Table
A systematic listing of all possible combinations of truth values for atomic propositions and the resulting truth values of compound expressions
Symbolic Representation
A formal system of notation using well-defined symbols to express logical relationships and operations with precision and clarity
Non-contradiction
The logical principle that asserts ¬(P ∧ ¬P) is always true. No statement can be both true and false in the same sense at the same time
Law of Excluded Middle
The principle that every proposition P is either true or false, formally expressed as P ∨ ¬P
Necessary and Sufficient Conditions
P is necessary for Q if Q → P, and P is sufficient for Q if P → Q. If both hold, then P ↔ Q
Propositional Calculus
A formal system dealing with propositions and logical connectives, where formulas are built from atomic propositions using logical operators
First-order Logic
A formal system extending propositional logic with quantifiers (∀, ∃) and predicates, allowing expression of relationships and properties
Higher-order Logic
A logical system allowing quantification over predicates, functions, and other higher-order objects, extending first-order logic's expressiveness
Interpretation
A mapping I from a formal language L to a domain D that assigns semantic meaning to the symbols and expressions of L. Written as I: L → D
Model Theory
Mathematical study of the relationship between formal theories T and their models M, where M ⊨ T denotes M is a model of T
Proof Theory
Study of formal proofs as mathematical objects and the structural relationships between them
String
A finite sequence s = a₁a₂...aₙ where each aᵢ belongs to an alphabet Σ. Formally written as s ∈ Σ*
Expression
A syntactically valid combination of symbols according to formation rules of a formal system
Elementary Proposition
An atomic statement P that has a truth value and cannot be decomposed into simpler logical statements
Syntax Tree
A hierarchical data structure T = (V,E,r) representing the grammatical structure of an expression, where V is the set of nodes, E the edges, and r the root
Node
A fundamental unit v ∈ V in a tree structure containing data and maintaining relationships with other nodes through edges E
Leaf Node
A terminal node l ∈ V in a tree structure with no children, formally: l ∈ V such that ∄v ∈ V: (l,v) ∈ E
Root Node
The unique node r ∈ V in a tree structure with no parent, serving as the origin point. Formally: r ∈ V such that ∄v ∈ V: (v,r) ∈ E
Branch
A directed edge e = (u,v) ∈ E in a tree structure connecting a parent node u to a child node v
Partial Proposition
An incomplete logical statement φ(x₁,...,xₙ) containing free variables or undefined terms that requires additional context to determine truth value
Complete Proposition
A logical statement p that is fully specified and has a well-defined truth value under any given interpretation I
Degree of Syntax Tree
The maximum number d of child nodes for any node v in the tree T. Formally: d = max{|children(v)| : v ∈ V}
Construction Sequence
An ordered sequence of steps S = (s₁, s₂, ..., sₙ) that, when executed in order, produces a valid logical structure or proof
Compound Proposition
A proposition p constructed by combining simpler propositions using logical connectives. Formally: p := q ∘ r where ∘ ∈ {∧, ∨, →, ↔}
Substitution
An operation σ that replaces variables or subexpressions with other expressions. Formally: σ: V → Terms where V is the set of variables
Structural Induction
A proof technique establishing that a property P holds for all instances of a recursively defined structure S by showing it holds for base cases and is preserved by construction steps
Absorption
A logical law stating that $P \land (P \lor Q) \equiv P$ and $P \lor (P \land Q) \equiv P$. Also known as the absorption laws in Boolean algebra.
Assignment, Valuation
A function $v: Vars \to D$ that assigns values from domain $D$ to variables in a logical expression, or more generally, an interpretation that maps symbols to their semantic values.
Bijection
A function $f: A \to B$ that is both injective (one-to-one) and surjective (onto). For every element $b \in B$, there exists exactly one element $a \in A$ such that $f(a) = b$.
Calculus
A formal system or method of reasoning in logic and mathematics. In logic, refers to various symbolic calculation systems like propositional calculus, predicate calculus, or lambda calculus.
Cardinality
The measure of the size of a set, denoted $|A|$ or $card(A)$. For finite sets, it's the number of elements. For infinite sets, it distinguishes different sizes of infinity.
Class
In set theory and logic, a collection of objects or elements that may be too large to form a set. Used to handle collections that would lead to paradoxes if considered as sets (like the class of all sets).
Clause
In logic, a disjunction of literals (atomic formulas or their negations). In propositional logic, a clause has the form $L_1 \lor L_2 \lor ... \lor L_n$ where each $L_i$ is a literal.
Closed formula (Sentence)
A formula with no free variables. All variables are bound by quantifiers or other binding operators. A sentence can be evaluated to true or false without additional context.
Closed term (Ground term)
A term containing no variables, only constants and function symbols. Ground terms represent specific objects in the domain without any unspecified parameters.
Compactness
A fundamental property of first-order logic stating that if every finite subset of a set of sentences Γ has a model, then the entire set Γ has a model. Formally: if Γ ⊨ φ, then there exists finite Γ₀ ⊆ Γ such that Γ₀ ⊨ φ.
