Logic Terms and Definitions
Errors in Logic(1)
Formal Language(2)
Formal Logic(17)
Foundations(5)
Inference Rules(4)
Logic(2)
Logic Basics(8)
Logical Connectives(11)
Logical Principles(4)
Proof Methods(5)
Quantifiers(2)
Reasoning(11)
Structures(6)
Truth Values(3)
AAbsorptionLogical PrinciplesAAntecedentLogical ConnectivesAArgumentReasoningAAssignment, ValuationFormal LogicAAxiomFoundationsBBiconditionalLogical ConnectivesBBijectionFoundationsBBound VariableLogic BasicsBBranchStructuresCCalculusFormal LogicCCardinalityFoundationsCClassFoundationsCClauseFormal LogicCClosed formula (Sentence)Formal LogicCClosed term (Ground term)Formal LogicCCompactnessFormal LogicCComplete PropositionLogic BasicsCCompound PropositionLogical ConnectivesCConclusionReasoningCConditionalLogical ConnectivesCConjunctionLogical ConnectivesCConjunctive Normal Form (CNF)LogicCConsequentLogical ConnectivesCConstruction SequenceProof MethodsCContradictionTruth ValuesDDeductionReasoningDDegree of Syntax TreeStructuresDDisjunctionLogical ConnectivesDDisjunctive Normal Form (DNF)LogicDDisjunctive SyllogismInference RulesEElementary PropositionLogic BasicsEEquivalenceLogical ConnectivesEExistential QuantifierQuantifiersEExpressionFormal LanguageFFallacyErrors in LogicFFirst-order LogicFormal LogicFFormal LanguageFormal LogicFFormal SystemFormal LogicHHigher-order LogicFormal LogicIImplicationLogical ConnectivesIInductionReasoningIInferenceReasoningIInterpretationFormal LogicLLaw of Excluded MiddleLogical PrinciplesLLeaf NodeStructuresLLogical ConnectiveLogical ConnectivesLLogical ConsequenceReasoningLLogical ConsistencyFormal LogicLLogical FormFormal LogicMModel TheoryFormal LogicMModus PonensInference RulesMModus TollensInference RulesNNatural DeductionProof MethodsNNecessary and Sufficient ConditionsLogical PrinciplesNNegationLogical ConnectivesNNodeStructuresNNon-contradictionLogical PrinciplesPPartial PropositionLogic BasicsPPredicateLogic BasicsPPremiseReasoningPProofReasoningPProof TheoryProof MethodsPPropositionLogic BasicsPPropositional CalculusFormal LogicQQuantifierLogic BasicsRRoot NodeStructuresRRule of InferenceInference RulesSSatisfiabilityFormal LogicSSequent CalculusProof MethodsSSoundnessReasoningSStringFormal LanguageSStructural InductionProof MethodsSSubstitutionReasoningSSymbolic RepresentationFormal LogicSSyntax TreeStructuresTTautologyTruth ValuesTTheoremFoundationsTTruth TableTruth ValuesUUnbound VariableLogic BasicsUUniversal QuantifierQuantifiersVValidityReasoning
81 of 81 terms
Errors in Logic
FallacyFormal Logic
SatisfiabilityLogical FormLogical ConsistencyFormal SystemFormal LanguageSymbolic RepresentationPropositional CalculusFirst-order LogicHigher-order LogicInterpretationModel TheoryAssignment, ValuationCalculusClauseClosed formula (Sentence)Closed term (Ground term)CompactnessLogic Basics
Bound VariableUnbound VariablePropositionPredicateQuantifierElementary PropositionPartial PropositionComplete PropositionLogical Connectives
ConjunctionDisjunctionConditionalAntecedentConsequentBiconditionalLogical ConnectiveImplicationEquivalenceNegationCompound PropositionLogical Principles
Non-contradictionLaw of Excluded MiddleNecessary and Sufficient ConditionsAbsorptionLogic Basics
Bound Variable
Definition:
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
- Cannot be freely substituted
- Value determined by quantifier
- Same variable can be bound differently in different scopes
Bound variables in:
∀x(x > 0): x is bound by ∀
∃y(y² = 2): y is bound by ∃
∫₀¹ x dx: x is bound by integral
Nested scopes:
∀x∃y(x < y): both x and y are bound
∀x(x > 0): x is bound by ∀
∃y(y² = 2): y is bound by ∃
∫₀¹ x dx: x is bound by integral
Nested scopes:
∀x∃y(x < y): both x and y are bound
Unbound Variable
Definition:
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
- Can be freely substituted
- Value not controlled by formula
- Must be specified externally
Free variables:
P(x): x is free
x + y = 5: both x and y are free
Mixed example:
∀x(P(x,y)): x is bound, y is free
P(x): x is free
x + y = 5: both x and y are free
Mixed example:
∀x(P(x,y)): x is bound, y is free
Proposition
Definition:
A declarative statement that is either true or false, but not both. Also called a propositional variable or atomic formula in formal logic.
- Must be declarative (not a question or command)
- Must be unambiguous
- Truth value is independent of observer
Valid propositions:
- "2 + 2 = 4"
- "Paris is the capital of France"
- "All integers greater than 2 are prime"
Not propositions:
- "x + 1 = 5" (variable statement)
- "How old are you?" (question)
- "Go to sleep" (command)
- "2 + 2 = 4"
- "Paris is the capital of France"
- "All integers greater than 2 are prime"
Not propositions:
- "x + 1 = 5" (variable statement)
- "How old are you?" (question)
- "Go to sleep" (command)
Predicate
Definition:
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.
- Returns a truth value when variables are specified
- Forms basis for quantified statements
- Domain must be specified for each variable
Single variable predicate:
P(x): "x is prime"
- P(2) is true
- P(4) is false
Two variable predicate:
Q(x,y): "x is greater than y"
- Q(5,3) is true
- Q(2,7) is false
P(x): "x is prime"
- P(2) is true
- P(4) is false
Two variable predicate:
Q(x,y): "x is greater than y"
- Q(5,3) is true
- Q(2,7) is false
Fundamental for expressing mathematical statements and forming basis for predicate logic and quantifiers
Quantifier
Definition:
A logical operator that specifies the quantity of specimens in a domain for which a predicate holds. Two main types: universal quantifier (∀: 'for all') and existential quantifier (∃: 'there exists')
- Has scope of application
- Can be nested
- Can be negated
Universal quantifier:
∀x(x2≥0) - "For all x, x squared is non-negative"
Existential quantifier:
∃x(x2=2) - "There exists x where x squared equals 2"
Combined quantifiers:
∀x∃y(y>x) - "For all x there exists y greater than x"
∀x(x2≥0) - "For all x, x squared is non-negative"
Existential quantifier:
∃x(x2=2) - "There exists x where x squared equals 2"
Combined quantifiers:
∀x∃y(y>x) - "For all x there exists y greater than x"
Negating quantifiers:
- ¬(∀x)P(x)≡∃x(¬P(x))
- ¬(∃x)P(x)≡∀x(¬P(x))
- ¬(∀x)P(x)≡∃x(¬P(x))
- ¬(∃x)P(x)≡∀x(¬P(x))
Elementary Proposition
Definition:
An atomic statement P that has a truth value and cannot be decomposed into simpler logical statements
- Atomic (indivisible)
- Truth-valued
- Independent
- Basic building block
- Binary truth value
- No internal logical structure
- Can be negated
- Combines with connectives
Basic Statements:
"It is raining"
"2 is prime"
"The sky is blue"
Counter-examples (not elementary):
"It is raining and cold" (compound)
"If x>0 then x²>0" (conditional)
"All numbers are positive" (quantified)
- Foundation for complex logic
- Truth table construction
- Propositional calculus
- Logical analysis
- Cannot express quantification
- No internal structure
- No predicates
- No variables
Partial Proposition
Definition:
An incomplete logical statement φ(x₁,...,xₙ) containing free variables or undefined terms that requires additional context to determine truth value
- Contains free variables
- Truth value undefined
- Context dependent
- Requires completion
- Open formulas
- Templates
- Schemata
- Placeholders
Predicate Logic:
P(x): "x is prime"
Q(x,y): "x is greater than y"
Templates:
"If ___, then ___"
"___ is a ___ of ___"
- Variable binding
- Substitution
- Context provision
- Quantification
Complete Proposition
Definition:
A logical statement p that is fully specified and has a well-defined truth value under any given interpretation I
- Has definite truth value
- No free variables
- Context independent
- Well-formed formula
- Ground formulas
- Closed formulas
- Sentences
- Full assertions
Atomic Propositions:
"2 is prime"
"Today is Monday"
"Water freezes at 0°C"
Compound Propositions:
"If it rains, then the ground is wet"
"All natural numbers are either even or odd"
"(2 + 2 = 4) ∧ (3 × 3 = 9)"
- Truth value determinable
- Interpretation independent
- Testable conditions
- Logical evaluation
Reasoning
Inference
Definition:
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
- Must follow valid rules of logic
- Preserves truth from premises to conclusion
- Can be direct or indirect
- Forms basis of mathematical proofs
Modus Ponens:
P₁: p → q
P₂: p
∴ q
Modus Tollens:
P₁: p → q
P₂: ¬q
∴ ¬p
P₁: p → q
P₂: p
∴ q
Modus Tollens:
P₁: p → q
P₂: ¬q
∴ ¬p
- Direct inference
- Conditional inference
- Deductive reasoning
- Inductive reasoning
- Transitive inference
Proof
Definition:
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
- Each step must be justified
- No circular reasoning allowed
- Assumptions must be stated clearly
- Must be complete and rigorous
- Proof by contradiction
- Proof by contrapositive
- Mathematical induction
- Proof by cases
- Existence proofs
- Uniqueness proofs
Standard format:
1. Given/Assumptions
2. Statement to prove
3. Logical steps
4. Therefore conclusion
1. Given/Assumptions
2. Statement to prove
3. Logical steps
4. Therefore conclusion
Direct proof example:
Prove: If n is even, then n² is even
Proof:
- Let n be even
- Then n = 2k for some integer k
- n² = (2k)² = 4k² = 2(2k²)
- Therefore n² is even
Prove: If n is even, then n² is even
Proof:
- Let n be even
- Then n = 2k for some integer k
- n² = (2k)² = 4k² = 2(2k²)
- Therefore n² is even
Premise
Definition:
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: CP1,P2,...,Pn
- Truth value must be known or assumed
- Can be axioms, definitions, or proven statements
- Independent of conclusion being proven
Syllogism premises:
P₁: All men are mortal
P₂: Socrates is a man
C: Therefore, Socrates is mortal
Logical form:
P₁: p → q
P₂: p
C: Therefore, q
P₁: All men are mortal
P₂: Socrates is a man
C: Therefore, Socrates is mortal
Logical form:
P₁: p → q
P₂: p
C: Therefore, q
- Minor premise (specific instance)
- Hidden/Implicit premises
- Axioms (taken as self-evident)
Conclusion
Definition:
The statement C derived from premises P₁, P₂, ..., Pₙ through valid logical inference. In formal notation: P₁, P₂, ..., Pₙ ⊢ C or CP1,P2,...,Pn
- Truth value depends on:
• Truth of premises
• Validity of inference rules
- Cannot contain new variables not in premises
- Strength depends on premise support
Valid conclusion:
P₁: If it rains, ground is wet
P₂: It is raining
C: Therefore, ground is wet
Formal logic:
P₁: p → q
P₂: p
C: ∴ q
P₁: If it rains, ground is wet
P₂: It is raining
C: Therefore, ground is wet
Formal logic:
P₁: p → q
P₂: p
C: ∴ q
A conclusion is valid if:
- Premises are true
- Rules of inference are correct
- No logical fallacies present
- Premises are true
- Rules of inference are correct
- No logical fallacies present
Validity
Definition:
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
- Depends only on logical structure
- Preserved through valid inference rules
- Different from soundness (valid + true premises)
Valid but not sound:
P₁: All cats are green
P₂: Whiskers is a cat
C: Therefore, Whiskers is green
(Valid structure, false premise)
Valid and sound:
P₁: All squares have 4 sides
P₂: Figure A is a square
C: Therefore, Figure A has 4 sides
P₁: All cats are green
P₂: Whiskers is a cat
C: Therefore, Whiskers is green
(Valid structure, false premise)
Valid and sound:
P₁: All squares have 4 sides
P₂: Figure A is a square
C: Therefore, Figure A has 4 sides
Ways to test validity:
- Truth tables
- Formal proofs
- Counter-example method
- Venn diagrams
- Truth tables
- Formal proofs
- Counter-example method
- Venn diagrams
Soundness
Definition:
The property of an argument being both valid and having true premises.
Argument
Definition:
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 CP1,P2,...,Pn
- Must have exactly one conclusion
- Can be valid or invalid
- Can be sound or unsound
- Form determines validity, not content
Deductive argument:
P₁: All mammals are warm-blooded
P₂: All dogs are mammals
C: Therefore, all dogs are warm-blooded
Symbolic form:
P₁: p → q
P₂: r → p
C: Therefore, r → q
P₁: All mammals are warm-blooded
P₂: All dogs are mammals
C: Therefore, all dogs are warm-blooded
Symbolic form:
P₁: p → q
P₂: r → p
C: Therefore, r → q
- Inductive (conclusion probable but not certain)
- Direct (straight line of reasoning)
- Indirect (proof by contradiction)
Deduction
Definition:
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.
- Moves from general to specific
- Truth-preserving when valid
- Conclusion certainty depends on premises
- Forms basis of mathematical proofs
- Modus Ponens: ((P → Q) ∧ P) ⊢ Q
- Modus Tollens: ((P → Q) ∧ ¬Q) ⊢ ¬P
- Hypothetical Syllogism: ((P → Q) ∧ (Q → R)) ⊢ (P → R)
Mathematical:
Premise 1: All integers divisible by 4 are even
Premise 2: 12 is divisible by 4
Conclusion: Therefore, 12 is even
Real-world:
Premise 1: All mammals are warm-blooded
Premise 2: Dogs are mammals
Conclusion: Therefore, dogs are warm-blooded
- Mathematical proofs
- Legal reasoning
- Computer programming
- Scientific hypothesis testing
Induction
Definition:
A method of reasoning that derives general principles from specific observations, establishing probable (not certain) conclusions.
- Moves from specific to general
- Conclusion extends beyond premises
- Results in probability, not certainty
- Subject to new evidence
- Simple Enumeration: observing pattern in instances
- Elimination: removing alternative explanations
- Analogy: reasoning from similar cases
- Statistical Inference: generalizing from samples
Mathematical:
Observation 1: 1 = 1
Observation 2: 1 + 2 = 3
Observation 3: 1 + 2 + 3 = 6
Conjecture: Sum of first n integers = n(n+1)/2
Scientific:
Observation: Every observed swan is white
Induction: Therefore, all swans are white
(Note: Shows limitation - black swans exist)
- Problem of induction (Hume)
- Cannot guarantee universal truth
- Susceptible to counterexamples
- Requires representative samples
Logical Consequence
Definition:
A statement φ is a logical consequence of premises Γ (written Γ ⊨ φ) if φ is true in every model where all premises in Γ are true
- Transitive: If A⊨B and B⊨C, then A⊨C
- Monotonic in classical logic
- Independent of syntax
- Preserved under substitution
- Semantic consequence (model-theoretic)
- Syntactic consequence (proof-theoretic)
- Material consequence
- Strict consequence
Semantic Consequence:
Premises:
- All humans are mortal
- Socrates is human
Consequence:
- Socrates is mortal
Material Consequence:
Premises:
- If it rains, streets are wet
- Streets are not wet
Consequence:
- It is not raining
- A ⊨ B iff A → B is valid
- Γ ⊨ φ iff Γ ⊢ φ (completeness)
- Truth preservation
- Necessity preservation
Substitution
Definition:
An operation σ that replaces variables or subexpressions with other expressions. Formally: σ: V → Terms where V is the set of variables
- Preserves well-formedness
- Compositional
- Type-preserving
- Capture-avoiding
- Variable substitution
- Term substitution
- Expression substitution
- Pattern substitution
Variable Substitution:
P(x) [x/a] = P(a)
Term Substitution:
(x + y)[x/(a+b)] = (a+b) + y
Formula Substitution:
(P → Q)[P/R∧S] = ((R∧S) → Q)
- Proof steps
- Equation solving
- Unification
- Pattern matching
Foundations
Axiom
Definition:
A statement accepted as true without proof in a logical system.
Theorem
Definition:
A statement that has been proven based on axioms and logical rules.
Bijection
Definition:
A function f:A→B that is both injective (one-to-one) and surjective (onto). For every element b∈B, there exists exactly one element a∈A such that f(a)=b.
- One-to-one correspondence
- Has inverse function
- Preserves cardinality
- Maps between sets of equal size
Identity Function:
f(x)=x is a bijection from R to R
Exponential Function:
f(x)=ex is a bijection from R to R+
Set Bijection:
f:{1,2,3}→{a,b,c} where f(1)=a,f(2)=b,f(3)=c
- Set theory cardinality
- Isomorphisms in algebra
- Cryptography
- Combinatorics
- Check injectivity: f(x1)=f(x2)⇒x1=x2
- Check surjectivity: ∀y∈B,∃x∈A:f(x)=y
- Construct inverse function
Cardinality
Definition:
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.
- Finite cardinality: ∣A∣=n for some n∈N
- Countably infinite: ∣A∣=ℵ0 (aleph-null)
- Uncountably infinite: ∣A∣>ℵ0
- ∣A∪B∣=∣A∣+∣B∣−∣A∩B∣ (finite sets)
- ∣A×B∣=∣A∣×∣B∣
- ∣P(A)∣=2∣A∣ (power set)
- Cantor's theorem: ∣A∣<∣P(A)∣
Finite Sets:
∣{1,2,3}∣=3
Infinite Sets:
∣N∣=ℵ0 (natural numbers)
∣R∣=2ℵ0 (real numbers)
∣P(N)∣=2ℵ0
- Set theory
- Combinatorics
- Measure theory
- Database theory
Class
Definition:
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).
- May be proper (not a set)
- Can contain sets as elements
- Avoids set-theoretic paradoxes
- Used in axiomatic set theory
- Proper classes: too large to be sets
- Small classes: actually sets
- Universal class: contains all objects
- Complement classes
Russell's Paradox Avoidance:
Class R = {x | x ∉ x} (class of all sets that don't contain themselves)
Class of All Sets:
V = {x | x = x} (cannot be a set in standard ZFC)
Set vs Class:
{1,2,3} is a set
{x | x is a set} is a proper class
- Foundation of set theory
- Category theory
- Mathematical logic
- Type theory
Errors In Logic
Fallacy
Definition:
A flaw or error in reasoning that renders an argument invalid.
Truth Values
Contradiction
Definition:
A statement that is always false regardless of the truth values of its components.
Tautology
Definition:
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
- Truth table shows all true results
- Used in proving logical equivalence
- Negation is a contradiction
Common tautologies:
- Law of excluded middle: p ∨ ¬p
- Double negation: p 𠪪p
- Modus ponens: ((p → q) ∧ p) → q
Truth table for p ∨ ¬p:
p | ¬p | p ∨ ¬p
T | F | T
F | T | T
- Law of excluded middle: p ∨ ¬p
- Double negation: p 𠪪p
- Modus ponens: ((p → q) ∧ p) → q
Truth table for p ∨ ¬p:
p | ¬p | p ∨ ¬p
T | F | T
F | T | T
Can be verified by:
- Truth tables
- Logical equivalences
- Formal proofs
- Truth tables
- Logical equivalences
- Formal proofs
Truth Table
Definition:
A systematic listing of all possible combinations of truth values for atomic propositions and the resulting truth values of compound expressions
- Input columns (atomic propositions)
- Intermediate columns (subexpressions)
- Output column (final result)
- 2ⁿ rows for n variables
- Validity checking
- Satisfiability testing
- Logical equivalence
- Circuit design
Simple AND (P ∧ Q):
P | Q | P ∧ Q
T | T | T
T | F | F
F | T | F
F | F | F
Implication (P → Q):
P | Q | P → Q
T | T | T
T | F | F
F | T | T
F | F | T
- Tautology detection
- Contradiction detection
- Equivalence checking
- Minimal forms
Inference Rules
Modus Ponens
Definition:
A fundamental rule of inference: given (P → Q) and P, we can deduce Q. Formally written as: QP→Q,P or (P → Q) ∧ P ⊢ Q
- Valid for any propositions P and Q
- Forms basis for direct proofs
- Cannot be applied in reverse
Logical form:
P₁: P → Q (If P then Q)
P₂: P (P is true)
C: Therefore, Q (Q must be true)
Real example:
P₁: If it rains, then streets are wet
P₂: It is raining
C: Therefore, streets are wet
P₁: P → Q (If P then Q)
P₂: P (P is true)
C: Therefore, Q (Q must be true)
Real example:
P₁: If it rains, then streets are wet
P₂: It is raining
C: Therefore, streets are wet
Used in:
- Mathematical proofs
- Programming logic
- Legal reasoning
- Everyday inference
- Mathematical proofs
- Programming logic
- Legal reasoning
- Everyday inference
Modus Tollens
Definition:
A rule of inference: given (P → Q) and ¬Q, we can deduce ¬P. Formally written as: ¬PP→Q,¬Q or (P → Q) ∧ ¬Q ⊢ ¬P
- Valid for any propositions P and Q
- Contrapositive of Modus Ponens
- Often used in proof by contradiction
Logical form:
P₁: P → Q (If P then Q)
P₂: ¬Q (Q is false)
C: Therefore, ¬P (P must be false)
Real example:
P₁: If it's raining, ground is wet
P₂: Ground is not wet
C: Therefore, it's not raining
P₁: P → Q (If P then Q)
P₂: ¬Q (Q is false)
C: Therefore, ¬P (P must be false)
Real example:
P₁: If it's raining, ground is wet
P₂: Ground is not wet
C: Therefore, it's not raining
Used in:
- Indirect proofs
- Scientific reasoning (falsification)
- Diagnostic reasoning
- Error detection
- Indirect proofs
- Scientific reasoning (falsification)
- Diagnostic reasoning
- Error detection
Disjunctive Syllogism
Definition:
A rule of inference: given (P ∨ Q) and ¬P, we can deduce Q. Formally written as: QP∨Q,¬P or (P ∨ Q) ∧ ¬P ⊢ Q
- Valid for any propositions P and Q
- Works with either disjunct being false
- Requires exclusive OR not necessary
Logical form:
P₁: P ∨ Q (Either P or Q)
P₂: ¬P (Not P)
C: Therefore, Q (Q must be true)
Real example:
P₁: Either it's day or night
P₂: It's not day
C: Therefore, it's night
P₁: P ∨ Q (Either P or Q)
P₂: ¬P (Not P)
C: Therefore, Q (Q must be true)
Real example:
P₁: Either it's day or night
P₂: It's not day
C: Therefore, it's night
Used in:
- Process of elimination
- Troubleshooting
- Decision making
- Case analysis
- Process of elimination
- Troubleshooting
- Decision making
- Case analysis
Rule Of Inference
Definition:
A pattern of reasoning Γ ⊢ φ that preserves truth, where Γ is a set of premises and φ is the conclusion
- Modus Ponens: P→Q, P ⊢ Q
- Modus Tollens: P→Q, ¬Q ⊢ ¬P
- Hypothetical Syllogism: P→Q, Q→R ⊢ P→R
- Disjunctive Syllogism: P∨Q, ¬P ⊢ Q
- Resolution: (P∨Q), (¬P∨R) ⊢ Q∨R
- And-Introduction: P, Q ⊢ P∧Q
- Or-Introduction: P ⊢ P∨Q
- Universal Instantiation: ∀xP(x) ⊢ P(a)
Modus Ponens Example:
1. If it rains, the ground is wet (P→Q)
2. It is raining (P)
Therefore: The ground is wet (Q)
Resolution Example:
1. Either John or Mary is guilty (P∨Q)
2. John is not guilty (¬P)
Therefore: Mary is guilty (Q)
- Truth-preserving
- Validity guaranteed
- Independent of content
- Formal correctness
Logical Connectives
Conjunction
Definition:
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
- Associative: (P ∧ Q) ∧ R ≡ P ∧ (Q ∧ R)
- Idempotent: P ∧ P ≡ P
- Identity: P ∧ true ≡ P
Truth table:
P | Q | P ∧ Q
T | T | T
T | F | F
F | T | F
F | F | F
Real example:
P: It's raining
Q: It's cold
P ∧ Q: It's raining and cold
P | Q | P ∧ Q
T | T | T
T | F | F
F | T | F
F | F | F
Real example:
P: It's raining
Q: It's cold
P ∧ Q: It's raining and cold
De Morgan's Law: ¬(P ∧ Q) ≡ ¬P ∨ ¬Q
Disjunction
Definition:
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)
- Associative: (P ∨ Q) ∨ R ≡ P ∨ (Q ∨ R)
- Idempotent: P ∨ P ≡ P
- Identity: P ∨ false ≡ P
Truth table:
P | Q | P ∨ Q
T | T | T
T | F | T
F | T | T
F | F | F
Real example:
P: It's sunny
Q: It's cloudy
P ∨ Q: It's either sunny or cloudy
P | Q | P ∨ Q
T | T | T
T | F | T
F | T | T
F | F | F
Real example:
P: It's sunny
Q: It's cloudy
P ∨ Q: It's either sunny or cloudy
De Morgan's Law: ¬(P ∨ Q) ≡ ¬P ∧ ¬Q
Conditional
Definition:
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
- Not commutative: P → Q ≢ Q → P
- Transitive: If P → Q and Q → R, then P → R
- Contrapositive equivalence: P → Q ≡ ¬Q → ¬P
- False antecedent: If P is false, P → Q is true (vacuously true)
- Negation: ¬(P → Q) ≡ P ∧ ¬Q
Mathematical:
P: n is even
Q: n² is even
P → Q: If n is even, then n² is even
Real-world:
P: It rains
Q: The ground is wet
P → Q: If it rains, then the ground is wet
P: n is even
Q: n² is even
P → Q: If n is even, then n² is even
Real-world:
P: It rains
Q: The ground is wet
P → Q: If it rains, then the ground is wet
Antecedent
Definition:
In a conditional statement P → Q, the antecedent P is the hypothesis or condition that implies the consequent
- Acts as the "if" part of an "if-then" statement
- Determines the domain or conditions under which the implication holds
- Can be simple (P) or compound (P ∧ R)
- Strength of antecedent affects the logical strength of the conditional
- Multiple antecedents can be combined: (P ∧ Q) → R
Mathematical:
In "If x > 0, then x² > 0"
Antecedent is "x > 0"
Real-world:
In "If it rains, then the ground is wet"
Antecedent is "it rains"
In "If x > 0, then x² > 0"
Antecedent is "x > 0"
Real-world:
In "If it rains, then the ground is wet"
Antecedent is "it rains"
Consequent
Definition:
In a conditional statement P → Q, the consequent Q is the conclusion or result that follows from the antecedent
- Acts as the "then" part of an "if-then" statement
- Need not be causally related to antecedent
- Can be simple (Q) or compound (Q ∨ R)
- Multiple consequents possible through conjunction
- Forms basis for modus ponens inference rule
Mathematical:
In "If x > 0, then x² > 0"
Consequent is "x² > 0"
Real-world:
In "If it rains, then the ground is wet"
Consequent is "the ground is wet"
In "If x > 0, then x² > 0"
Consequent is "x² > 0"
Real-world:
In "If it rains, then the ground is wet"
Consequent is "the ground is wet"
Biconditional
Definition:
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)
- Commutative: P ↔ Q ≡ Q ↔ P
- Transitive: If P ↔ Q and Q ↔ R, then P ↔ R
- Equivalence relation: defines logical equivalence
- Stronger than simple conditional: requires both directions
- P ↔ Q ≡ (P → Q) ∧ (Q → P)
- P ↔ Q ≡ (P ∧ Q) ∨ (¬P ∧ ¬Q)
- ¬(P ↔ Q) ≡ P ⊕ Q (exclusive or)
Mathematical:
P: x² = 4
Q: x = ±2
P ↔ Q: x² = 4 if and only if x = ±2
Real-world:
P: Today is a weekend
Q: Today is Saturday or Sunday
P ↔ Q: Today is a weekend if and only if it's Saturday or Sunday
Logical Connective
Definition:
Operators that combine simple propositions into compound propositions, forming the basic building blocks of logical expressions
- Unary connectives: negation (¬)
- Binary connectives: conjunction (∧), disjunction (∨)
- Implications: conditional (→), biconditional (↔)
- Other: exclusive or (⊕), NAND (↑), NOR (↓)
- Truth-functionality: output determined by inputs
- Completeness: some sets of connectives are functionally complete
- Interdefinability: connectives can define each other
- Precedence: standard order of operations
Basic Combinations:
P ∧ Q: Conjunction (AND)
P ∨ Q: Disjunction (OR)
¬P: Negation (NOT)
P → Q: Implication (IF-THEN)
P ↔ Q: Biconditional (IF AND ONLY IF)
- {¬, ∧} is functionally complete
- {¬, ∨} is functionally complete
- {↑} (NAND) is functionally complete alone
- {↓} (NOR) is functionally complete alone
- Digital circuit design
- Programming language operators
- Database queries
- Artificial intelligence logic
Implication
Definition:
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.
- Not commutative: P → Q ≢ Q → P
- Not associative: (P → Q) → R ≢ P → (Q → R)
- Equivalent to ¬P ∨ Q
- Vacuously true when P is false
- Material implication: truth-functional P → Q
- Strict implication: necessarily P → Q
- Counterfactual: if P were true, Q would be true
- Causal implication: P causes Q
Mathematical:
P: n is prime
Q: n has exactly two factors
P → Q: If n is prime, then n has exactly two factors
Real-world:
P: It is raining
Q: The ground is wet
P → Q: If it is raining, then the ground is wet
- Modus Ponens: ((P → Q) ∧ P) ⊢ Q
- Modus Tollens: ((P → Q) ∧ ¬Q) ⊢ ¬P
- Hypothetical Syllogism: ((P → Q) ∧ (Q → R)) ⊢ (P → R)
P | Q | P → Q
T | T | T
T | F | F
F | T | T
F | F | T
- Affirming the consequent: ((P → Q) ∧ Q) ⊬ P
- Denying the antecedent: ((P → Q) ∧ ¬P) ⊬ ¬Q
- Mistaking correlation for causation
Equivalence
Definition:
Two logical statements p and q are equivalent (p≡q) if they have identical truth values under all possible valuations of their variables
- p≡p
- Symmetric: if p≡q then q≡p
- Transitive: if p≡q and q≡r then p≡r
Common equivalences:
p→q≡¬p∨q
(p∧q)≡¬(¬p∨¬q) (De Morgan's Law)
¬¬p≡p (Double Negation)
p→q≡¬p∨q
(p∧q)≡¬(¬p∨¬q) (De Morgan's Law)
¬¬p≡p (Double Negation)
Can be proven using truth tables or logical proofs
Negation
Definition:
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.
- Involution: ¬(¬P) ≡ P (double negation law)
- Contradictions: P ∧ ¬P is always false
- Tautologies: P ∨ ¬P is always true
- Basic completeness: {¬, ∧} or {¬, ∨} are functionally complete
- De Morgan's Laws:
¬(P ∧ Q) ≡ ¬P ∨ ¬Q
¬(P ∨ Q) ≡ ¬P ∧ ¬Q
- Implication: ¬(P → Q) ≡ P ∧ ¬Q
- Biconditional: ¬(P ↔ Q) ≡ P ⊕ Q
Mathematical:
P: x > 0
¬P: x ≤ 0
Logical:
P: All ravens are black
¬P: Some ravens are not black
Real-world:
P: It is raining
¬P: It is not raining
- Proof by contradiction
- Boolean algebra
- Digital circuit design
- Database queries
Compound Proposition
Definition:
A proposition p constructed by combining simpler propositions using logical connectives. Formally: p := q ∘ r where ∘ ∈ {∧, ∨, →, ↔}
- Simple propositions
- Logical connectives
- Grouping symbols
- Precedence rules
- Binary connective usage
- Unary negation
- Proper parenthesization
- Well-formed combinations
Basic Forms:
P ∧ Q (conjunction)
P ∨ Q (disjunction)
P → Q (implication)
Complex Forms:
(P ∧ Q) → R
¬(P ∨ Q) ∧ (R → S)
(P → Q) ↔ (¬Q → ¬P)
- Truth-functional
- Component-based
- Precedence-respecting
- Context-independent
Logic
Disjunctive Normal Form (DNF)
Definition:
A logical formula is in DNF if it is a disjunction (OR) of conjunctions (AND) of literals (variables or their negations): (p∧q)∨(¬p∧r)∨(q∧r)
- Every formula can be converted to DNF
- Each conjunction is a minterm
- No conjunction contains both a variable and its negation
- No distributive laws needed after conversion
Converting to DNF:
Complex example:
(p→q)≡(¬p∨q)
(p↔q)≡(p∧q)∨(¬p∧¬q)
Complex example:
¬(p∧q)≡(¬p∨¬q)
Conjunctive Normal Form (CNF)
Definition:
A logical formula is in CNF if it is a conjunction (AND) of disjunctions (OR) of literals (variables or their negations): (p∨q)∧(¬p∨r)∧(q∨r)
- Every formula can be converted to CNF
- Each disjunction is a maxterm
- No disjunction contains both a variable and its negation
- Useful in automated theorem proving
Converting to CNF:
Complex example:
(p→q)≡(¬p∨q)
(p↔q)≡(p∨¬q)∧(¬p∨q)
Complex example:
¬(p∨q)≡(¬p∧¬q)
Quantifiers
Universal Quantifier
Definition:
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)'
- Distributes over conjunction: ∀x(P(x) ∧ Q(x)) ≡ ∀xP(x) ∧ ∀xQ(x)
- Does not distribute over disjunction: ∀x(P(x) ∨ Q(x)) ≢ ∀xP(x) ∨ ∀xQ(x)
- Ordering matters with different quantifiers
- Empty domain: ∀xP(x) is vacuously true
- ¬(∀xP(x)) ≡ ∃x¬P(x)
- Double negation: ¬(¬(∀xP(x))) ≡ ∀xP(x)
- Important in proofs by contradiction
Mathematical:
∀x(x² ≥ 0) - For all real numbers, their square is non-negative
Set Theory:
∀x(x ∈ ℕ → x + 1 ∈ ℕ) - Natural numbers are closed under addition by 1
Real-world:
∀x(x is a mammal → x is warm-blooded)
"All mammals are warm-blooded"
- Mathematical theorems
- Logical necessity
- Set theory axioms
- Database queries
Existential Quantifier
Definition:
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)'
- Distributes over disjunction: ∃x(P(x) ∨ Q(x)) ≡ ∃xP(x) ∨ ∃xQ(x)
- Does not distribute over conjunction: ∃x(P(x) ∧ Q(x)) ≢ ∃xP(x) ∧ ∃xQ(x)
- Can be defined using universal quantifier and negation
- Empty domain: ∃xP(x) is false
- ¬(∃xP(x)) ≡ ∀x¬P(x)
- Double negation: ¬(¬(∃xP(x))) ≡ ∃xP(x)
- Used in constructive proofs
Mathematical:
∃x(x² = 2) - There exists a number whose square is 2
Set Theory:
∃x(x ∈ ℕ ∧ x + 1 = 1) - There exists a natural number that when added to 1 equals 1
Real-world:
∃x(x is a planet ∧ x has rings)
"There exists a planet that has rings"
- ∃!x P(x): exactly one element satisfies P
- ∃x(P(x) ∧ ∀y(P(y) → y = x))
- Important in mathematical definitions
Formal Logic
Satisfiability
Definition:
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
- NP-complete problem (SAT)
- Related to validity: φ valid ⇔ ¬φ unsatisfiable
- Independent of syntax
- Preserved under logical equivalence
- Boolean Satisfiability (SAT)
- Horn-SAT (conjunction of Horn clauses)
- 2-SAT (clauses with at most 2 literals)
- 3-SAT (clauses with at most 3 literals)
Satisfiable Formula:
(P ∨ Q) ∧ (¬P ∨ R)
Satisfied by P=true, Q=false, R=true
Unsatisfiable Formula:
P ∧ ¬P
No assignment can make this true
- Automated theorem proving
- Circuit design verification
- Constraint satisfaction
- Planning problems
Logical Form
Definition:
The underlying structure of a logical statement abstracted from its specific content, revealing the logical relationships between its components.
- Atomic propositions
- Logical connectives
- Quantifiers
- Variables and constants
- Predicates and relations
- Reveals logical structure
- Enables formal analysis
- Facilitates proof construction
- Shows logical equivalence
Natural Language:
"All humans are mortal and Socrates is human"
Logical Form:
(∀x(H(x) → M(x))) ∧ H(s)
Natural Language:
"Either it's raining or someone left the sprinkler on"
Logical Form:
R ∨ ∃x(P(x) ∧ S(x))
- Standardization of variables
- Removal of ambiguity
- Explicit quantifier scope
- Prenex normal form
- Skolemization
Logical Consistency
Definition:
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 ⊨ φ₁ ∧ φ₂ ∧ ... ∧ φₙ)
- Binary property of sets of statements
- Independent of actual truth values
- Preserved under logical equivalence
- Related to satisfiability of conjunction
- Truth table analysis
- Model finding
- Proof by contradiction
- Semantic tableaux
Consistent Set:
1. All birds can fly
2. Penguins are birds
3. Some birds cannot fly
(Consistent because not all birds must fly)
Inconsistent Set:
1. All birds can fly
2. Penguins are birds
3. Penguins cannot fly
4. All penguins must be able to fly
(Contradicts itself about penguins' ability to fly)
- Database integrity
- Knowledge base verification
- Legal reasoning
- Scientific theory development
Formal System
Definition:
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 (syntax)
- Formation rules
- Transformation rules
- Axioms or axiom schemas
- Inference rules
- Consistency: no contradictions derivable
- Completeness: all truths derivable
- Soundness: only valid conclusions derivable
- Decidability: existence of decision procedure
Propositional Logic:
- Language: P, Q, R, ∧, ∨, ¬, →, (, )
- Axioms: P∨¬P, (P→Q)→((Q→R)→(P→R))
- Rules: Modus Ponens
Peano Arithmetic:
- Language: 0, S, +, ×, =
- Axioms: ∀x(S(x)≠0), ∀x∀y(S(x)=S(y)→x=y)
- Rules: Mathematical induction
- Mathematical logic
- Programming language semantics
- Automated theorem proving
- Type theory
Formal Language
Definition:
A set of strings over an alphabet Σ, defined by precise formation rules. L ⊆ Σ*
- Alphabet (set of symbols)
- Grammar rules
- Well-formed formulas
- Syntax rules
- Semantics (interpretation)
- Regular languages
- Context-free languages
- Context-sensitive languages
- Recursively enumerable languages
Propositional Logic:
Alphabet: {P, Q, R, ∧, ∨, ¬, →, (, )}
WFF: P∧Q, (P→Q)∨R, ¬(P∧¬Q)
First-Order Logic:
Alphabet: {∀, ∃, P, f, x, y, =, ∧, ∨, ¬}
WFF: ∀x∃yP(x,y), ∀x(P(x)→Q(x))
- Programming languages
- Logic systems
- Compiler design
- Protocol specification
Symbolic Representation
Definition:
A formal system of notation using well-defined symbols to express logical relationships and operations with precision and clarity
- Propositional variables: P, Q, R
- Logical connectives: ∧, ∨, ¬, →, ↔
- Quantifiers: ∀, ∃
- Grouping symbols: (, ), [, ]
- Polish notation (prefix)
- Reverse Polish notation (postfix)
- Infix notation
- Abstract syntax trees
Classical Expression:
((P → Q) ∧ P) → Q
Polish Notation:
→∧→PQP Q
Abstract Syntax Tree:
→
∧ Q
→P P
- Unambiguous interpretation
- Formal manipulation rules
- Computer processability
- Mathematical rigor
Propositional Calculus
Definition:
A formal system dealing with propositions and logical connectives, where formulas are built from atomic propositions using logical operators
- Atomic propositions: P, Q, R...
- Logical connectives: ∧, ∨, ¬, →, ↔
- Well-formed formulas (WFF)
- Inference rules
- Axiom schemas
- Decidable
- Sound and complete
- Compact
- Truth-functional
Basic WFFs:
P ∧ Q
¬(P ∨ Q) → R
(P → Q) ↔ (¬Q → ¬P)
Natural Language:
"If it rains (P) and it's cold (Q), then I'll stay home (R)"
Formalized: (P ∧ Q) → R
- Digital circuit design
- Boolean algebra
- Program verification
- Expert systems
First-order Logic
Definition:
A formal system extending propositional logic with quantifiers (∀, ∃) and predicates, allowing expression of relationships and properties
- Variables: x, y, z...
- Constants: a, b, c...
- Predicates: P(x), Q(x,y)...
- Functions: f(x), g(x,y)...
- Quantifiers: ∀, ∃
- Terms: variables, constants, functions
- Atomic formulas: predicates applied to terms
- Quantified formulas: ∀x P(x), ∃x P(x)
- Complex formulas: combinations with connectives
Mathematical:
"Every natural number has a successor"
∀x∃y(S(y,x))
Real-world:
"Some student knows all topics"
∃x(Student(x) ∧ ∀y(Topic(y) → Knows(x,y)))
- Cannot quantify over predicates
- Cannot express finite cardinality directly
- Some mathematical concepts require schemas
- Not categorical for infinite structures
Higher-order Logic
Definition:
A logical system allowing quantification over predicates, functions, and other higher-order objects, extending first-order logic's expressiveness
- Predicate quantification
- Function quantification
- Type hierarchy
- Lambda abstraction
- Second-order: quantification over sets/predicates
- Third-order: quantification over sets of sets
- ω-order: arbitrary finite orders
- Type theory connection
Second-order:
"Every non-empty property has a minimal element"
∀P((∃xP(x)) → (∃y(P(y) ∧ ∀z(P(z) → y≤z))))
Set theory:
"Two sets are equal if they have the same elements"
∀X∀Y(∀z(z∈X ↔ z∈Y) → X=Y)
- Mathematical foundations
- Type theory
- Program verification
- Category theory
Limitations:
- Incomplete semantics
- Undecidable
- Model-theoretic complexity
Interpretation
Definition:
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
- Domain (universe of discourse)
- Function symbols interpretation
- Predicate symbols interpretation
- Constant symbols interpretation
- Truth value assignment
- Homomorphic structure
- Preserves logical operations
- Unique evaluation of terms
- Satisfaction relation (⊨)
Arithmetic Interpretation:
Domain: Natural numbers
0: zero element
S: successor function
+: addition function
×: multiplication function
Set-theoretic Interpretation:
Domain: Power set of natural numbers
∈: membership relation
∪: union operation
∩: intersection operation
- Model checking
- Semantics definition
- Consistency proofs
- Theory comparison
Model Theory
Definition:
Mathematical study of the relationship between formal theories T and their models M, where M ⊨ T denotes M is a model of T
- Satisfaction (⊨)
- Elementary equivalence
- Theory completeness
- Model completeness
- Compactness Theorem
- Löwenheim-Skolem Theorems
- Completeness Theorem
- Preservation Theorems
Field Theory:
- Real numbers as model
- Complex numbers as model
- Finite fields as models
Group Theory:
- Symmetric groups
- Cyclic groups
- Matrix groups
- Mathematical logic
- Universal algebra
- Algebraic geometry
- Computer science
- Elementary chains
- Ultraproducts
- Back-and-forth construction
- Model companions
Assignment, Valuation
Definition:
A function v:Vars→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.
- Maps variables to values
- Determines truth value of formulas
- Can be partial or total
- Domain-dependent
- Variable assignment function
- Truth value computation
- Model specification
- Interpretation mapping
Propositional Assignment:
v(P)=true,v(Q)=false
Then v(P∧Q)=false
Arithmetic Assignment:
v(x)=3,v(y)=5
Then v(x+y=8)=true
- Truth table construction
- Model checking
- Satisfiability testing
- Expression evaluation
Calculus
Definition:
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.
- Propositional calculus
- Predicate calculus
- Lambda calculus
- Modal calculus
- Process calculus
- Syntax rules
- Formation rules
- Inference rules
- Axioms or axiom schemas
Propositional Calculus:
Axioms: P→(Q→P)
Rules: Modus Ponens
Lambda Calculus:
Terms: variables, abstraction (λx.M), application (MN)
Rules: α-conversion, β-reduction
- Formal logic
- Programming language theory
- Mathematical proof systems
- Computer science foundations
Clause
Definition:
In logic, a disjunction of literals (atomic formulas or their negations). In propositional logic, a clause has the form L1∨L2∨...∨Ln where each Li is a literal.
- Disjunction of literals
- Basic unit in CNF
- Used in resolution
- Can be empty (contradiction)
- Unit clause: single literal
- Positive clause: no negated literals
- Negative clause: all literals negated
- Horn clause: at most one positive literal
Simple Clause:
P∨¬Q∨R
Unit Clause:
P (just one literal)
Empty Clause:
□ (contradiction)
Horn Clause:
¬P∨¬Q∨R (at most one positive literal)
- Resolution theorem proving
- SAT solvers
- Logic programming
- Automated reasoning
Closed Formula (Sentence)
Definition:
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.
- No free variables
- Truth value determined
- Context independent
- Can be proven or disproven
Predicate Logic Sentences:
∀x(P(x)→Q(x)) - all variables bound
∃y∀x(R(x,y)) - all variables quantified
Mathematical Sentences:
∀n∈N(n+0=n)
∃x∈R(x2=2)
Not Sentences (have free variables):
P(x)∧Q(y) - x and y are free
x+y=5 - x and y are free
- Check all variables are bound
- Verify quantifier scope
- Ensure no free occurrences
- Context-free evaluation
Closed Term (Ground Term)
Definition:
A term containing no variables, only constants and function symbols. Ground terms represent specific objects in the domain without any unspecified parameters.
- Contains no variables
- Fully specified
- Represents specific objects
- Can be evaluated concretely
Arithmetic Ground Terms:
2+3 (no variables)
f(a,b) where a, b are constants
sin(π/2) (mathematical constant)
Logical Ground Terms:
John (constant)
mother(Mary) where Mary is constant
add(succ(zero), succ(zero))
Not Ground Terms:
x+2 (contains variable x)
f(x,y) (contains variables x, y)
- Term rewriting systems
- Logic programming facts
- Automated theorem proving
- Database queries
Compactness
Definition:
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 Γ₀ ⊨ φ.
- Finite character property
- Applies to first-order logic
- Not true for second-order logic
- Fundamental metalogical result
- Löwenheim-Skolem theorems
- Existence of non-standard models
- Model construction techniques
- Upward/downward model transfer
Non-standard Analysis:
{x>n | n∈ℕ} ∪ standard axioms of ℝ
This has a model with infinitely large numbers
Graph Theory:
{Gₙ: "graph has cycles of length >n" | n∈ℕ}
By compactness, some graph has arbitrarily long cycles
Field Theory:
{pₙ=0 | pₙ prime} ∪ field axioms
Result: fields with characteristic 0 exist
- Model theory
- Non-standard analysis
- Algebraic logic
- Proof theory
Proof Methods
Natural Deduction
Definition:
A proof system that models logical reasoning through introduction and elimination rules for logical connectives. Proofs are trees of judgments Γ ⊢ φ
- Introduction rules (I-rules)
- Elimination rules (E-rules)
- Structural rules
- Derived rules
- ∧-Introduction: P, Q ⊢ P∧Q
- ∨-Elimination: P∨Q, [P⊢R], [Q⊢R] ⊢ R
- →-Introduction: [P⊢Q] ⊢ P→Q
- ∀-Introduction: [a]⊢P(a) ⊢ ∀xP(x)
Proof of P∧Q ⊢ Q∧P:
1. P∧Q (premise)
2. P (∧-elimination)
3. Q (∧-elimination)
4. Q∧P (∧-introduction)
Proof of P, P→Q ⊢ Q:
1. P (premise)
2. P→Q (premise)
3. Q (→-elimination)
- Local rules
- Assumption management
- Normal forms
- Cut elimination
Sequent Calculus
Definition:
A formal proof system using sequents of the form Γ ⊢ Δ, where Γ and Δ are finite multisets of formulas. Read as 'Γ entails Δ'
- Left rules (operating on Γ)
- Right rules (operating on Δ)
- Structural rules (weakening, contraction)
- Cut rule (transitivity of entailment)
- Cut elimination theorem
- Subformula property
- Decidability for propositional logic
- Conservative extension
Basic Rules:
Axiom: A ⊢ A
Cut: (Γ ⊢ Δ,A) and (A,Π ⊢ Λ) implies (Γ,Π ⊢ Δ,Λ)
Sample Derivation:
1. P ⊢ P (axiom)
2. P,Q ⊢ P (weakening)
3. P,Q ⊢ P∨Q (∨-right)
- Proof theory
- Automated theorem proving
- Type systems
- Program verification
Proof Theory
Definition:
Study of formal proofs as mathematical objects and the structural relationships between them
- Formal proof systems
- Proof normalization
- Cut elimination
- Proof search
- Natural deduction
- Sequent calculus
- Hilbert systems
- Resolution calculus
- Normalization theorem
- Cut-elimination theorem
- Herbrand's theorem
- Consistency proofs
- Automated theorem proving
- Program verification
- Type theory
- Constructive mathematics
- Structural induction
- Proof transformation
- Term rewriting
- Proof mining
Natural Deduction:
Proof of A∧B ⊢ B∧A
1. A∧B premise
2. A ∧-elimination
3. B ∧-elimination
4. B∧A ∧-introduction
Sequent Calculus:
Proof of ⊢ A→(B→(A∧B))
1. A,B ⊢ A axiom
2. A,B ⊢ B axiom
3. A,B ⊢ A∧B ∧-right
4. A ⊢ B→(A∧B) →-right
5. ⊢ A→(B→(A∧B)) →-right
Construction Sequence
Definition:
An ordered sequence of steps S = (s₁, s₂, ..., sₙ) that, when executed in order, produces a valid logical structure or proof
- Initial state
- Transformation rules
- Intermediate states
- Final state
- Well-defined steps
- Preserves validity
- Deterministic
- Finite length
Formula Construction:
1. Start with P
2. Add conjunction: P ∧
3. Add second operand: P ∧ Q
4. Add parentheses: (P ∧ Q)
Proof Construction:
1. State premises
2. Apply inference rule
3. State intermediate conclusion
4. Repeat until goal reached
- Proof building
- Expression parsing
- Tree construction
- Formula generation
Structural Induction
Definition:
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
- Base case(s)
- Inductive hypothesis
- Construction rules
- Inductive step
- Prove for atomic elements
- Assume for substructures
- Prove for composite
- Consider all constructions
List Induction:
Base: P(empty list)
Step: P(list) → P(cons(x,list))
Tree Induction:
Base: P(leaf)
Step: P(left) ∧ P(right) → P(node(left,right))
Formula Induction:
Base: P(atomic formulas)
Step: P(φ) ∧ P(ψ) → P(φ∘ψ)
- Data structure properties
- Program correctness
- Grammar validation
- Type systems
Logical Principles
Non-contradiction
Definition:
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
- Foundational to classical logic
- Related to consistency
- Independent of excluded middle
- Preserved under substitution
- Propositional: ¬(P ∧ ¬P)
- Predicate: ¬∃x(P(x) ∧ ¬P(x))
- Modal: □¬(P ∧ ¬P)
- Semantic: not(P is true and P is false)
Classical:
"A circle cannot be both round and not round"
Mathematical:
"A number cannot be both prime and composite"
Logical:
"A proposition cannot be both true and false"
- Aristotelian foundation
- Intuitionistic acceptance
- Dialectical challenges
- Quantum interpretations
Law Of Excluded Middle
Definition:
The principle that every proposition P is either true or false, formally expressed as P ∨ ¬P
- Tautology in classical logic
- Not accepted in intuitionistic logic
- Independent of non-contradiction
- Basis for proof by contradiction
- Propositional: P ∨ ¬P
- Predicate: ∀x(P(x) ∨ ¬P(x))
- Modal: □(P ∨ ¬P)
- Semantic: P is true or P is false
Classical:
"Either it is raining or it is not raining"
Mathematical:
"A number is either prime or not prime"
Set Theory:
"An element is either in a set or not in a set"
- Proof by contradiction
- Classical mathematics
- Boolean algebra
- Digital logic
Necessary And Sufficient Conditions
Definition:
P is necessary for Q if Q → P, and P is sufficient for Q if P → Q. If both hold, then P ↔ Q
- Necessary: Q cannot be true without P being true
- Sufficient: P being true guarantees Q is true
- Necessary and Sufficient: P ↔ Q (biconditional)
- Neither: P and Q are logically independent
- Necessary: Q → P
- Sufficient: P → Q
- Both: P ↔ Q
- Neither: No logical connection
Mathematical:
Being a square is sufficient (but not necessary) for being a rectangle
Having four equal sides is necessary (but not sufficient) for being a square
Being divisible by both 2 and 3 is necessary and sufficient for being divisible by 6
Real-world:
Being 18 is necessary (but not sufficient) for voting
Having a valid passport is sufficient (but not necessary) for ID
Being a US citizen and 35+ years old is necessary and sufficient for presidential eligibility
- Mathematical proofs
- Legal reasoning
- Scientific explanation
- Policy analysis
Absorption
Definition:
A logical law stating that P∧(P∨Q)≡P and P∨(P∧Q)≡P. Also known as the absorption laws in Boolean algebra.
- Simplifies redundant expressions
- Preserves truth values
- Commutative variants exist
- Applies to both conjunction and disjunction
Conjunction Form:
P∧(P∨Q)≡P
"It's raining AND (it's raining OR it's cold)" simplifies to "It's raining"
Disjunction Form:
P∨(P∧Q)≡P
"It's raining OR (it's raining AND it's cold)" simplifies to "It's raining"
- Boolean algebra simplification
- Logic circuit optimization
- Propositional logic simplification
- Set theory operations
Formal Language
String
Definition:
A finite sequence s = a₁a₂...aₙ where each aᵢ belongs to an alphabet Σ. Formally written as s ∈ Σ*
- Has finite length |s|
- Can be empty (ε)
- Can be concatenated
- Has substrings
- Concatenation (s₁·s₂)
- Reversal (sᴿ)
- Substring extraction
- Length computation
Over alphabet Σ = {a,b}:
Empty string: ε
Simple strings: a, ab, baa
Concatenation: ab·ba = abba
In formal logic:
Well-formed formula: (P∧Q)→R
Not well-formed: )P∧(
- Formal languages
- Pattern matching
- Computability theory
- Programming languages
Expression
Definition:
A syntactically valid combination of symbols according to formation rules of a formal system
- Atomic expressions
- Compound expressions
- Well-formed formulas
- Terms and formulas
- Constants
- Variables
- Operators
- Delimiters
- Functions
Logical Expressions:
P ∧ (Q ∨ R)
∀x(P(x) → Q(x))
Mathematical Expressions:
2x + 3y = 5
∫₀¹ x² dx
- Precedence rules
- Scope rules
- Type rules
- Syntactic categories
- Well-formedness
- Unambiguous parsing
- Type correctness
- Semantic meaning
Structures
Syntax Tree
Definition:
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
- Hierarchical structure
- Unique root node
- Directed edges
- Preserves operator precedence
- Abstract syntax trees (AST)
- Parse trees
- Derivation trees
- Expression trees
- Compiler design
- Expression evaluation
- Language processing
- Proof representation
Node
Definition:
A fundamental unit v ∈ V in a tree structure containing data and maintaining relationships with other nodes through edges E
- Contains data/value
- Has parent (except root)
- May have children
- Has depth/level
- Root node
- Internal nodes
- Leaf nodes
- Operator nodes
- Parent-child
- Siblings
- Ancestors
- Descendants
Logical Operators:
Node(∧): connects conjuncts
Node(∨): connects disjuncts
Node(¬): unary negation
Expression Trees:
Node(+): addition operator
Node(2): numeric literal
Node(x): variable
- Node creation
- Child addition/removal
- Value modification
- Tree traversal
Leaf Node
Definition:
A terminal node l ∈ V in a tree structure with no children, formally: l ∈ V such that ∄v ∈ V: (l,v) ∈ E
- No children
- Terminal element
- Contains atomic data
- Always has parent (except if root)
- Degree = 0
- Terminal in traversal
- Contains primitive values
- Cannot be expanded
In Expression Trees:
- Variables (x, y, z)
- Constants (2, 3.14, true)
- Atomic propositions (P, Q, R)
In Parse Trees:
- Tokens
- Literals
- Identifiers
- Terminal symbols
- Expression evaluation
- Tree traversal endpoints
- Pattern matching
- Value storage
Root Node
Definition:
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
- No parent node
- Unique in tree
- Level/depth 0
- Ancestor of all nodes
- Entry point for traversal
- Contains main operator/function
- Defines scope/context
- Maximum in partial ordering
Expression Trees:
P ∧ (Q ∨ R):
Root = ∧ (main connective)
Function Application:
f(g(x)):
Root = f (outermost function)
Arithmetic:
(2 + 3) × 4:
Root = × (last operation)
- Tree initialization
- Subtree access
- Structure modification
- Tree rebalancing
Branch
Definition:
A directed edge e = (u,v) ∈ E in a tree structure connecting a parent node u to a child node v
- Directed relationship
- Unique parent end
- Weight/cost possible
- Represents hierarchy
- Left branch
- Right branch
- Ordered branches
- Weighted branches
Binary Operations:
∧-branches: connect to both operands
¬-branch: connects to single operand
Function Application:
f(x,y): two branches to arguments
Parse Trees:
IF-THEN: branches to condition and body
- Branch creation
- Branch deletion
- Path traversal
- Tree restructuring
Degree Of Syntax Tree
Definition:
The maximum number d of child nodes for any node v in the tree T. Formally: d = max{|children(v)| : v ∈ V}
- Fixed for specific types
- Affects tree balance
- Influences traversal
- Impacts complexity
- Binary trees (d=2)
- Ternary trees (d=3)
- N-ary trees
- Variable degree trees
Logical Operators:
¬ (degree 1)
∧,∨,→,↔ (degree 2)
IF-THEN-ELSE (degree 3)
Function Application:
f(x) (degree 1)
g(x,y) (degree 2)
h(x,y,z) (degree 3)
- Storage requirements
- Processing efficiency
- Tree balancing
- Algorithm design