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
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
