Quantificational Logic Calculator info

Quantifiable logic or in the cotext of this app First-Order Logic, often abbreviated as FOL, is a branch of logic that extends Propositional Logic. It deals with propositions (statements) that are either true or false, similar to Propositional Logic. However, it goes further by introducing variables, predicates, quantifiers, and functions, allowing for more complex and expressive statements. In this app, you can generate natural deduction proofs for FOL containing universal and existential quantifiers.

For more detailed information, see Wikipedia

See Quantificational Logic Calculator here

Input Syntax

All uppercase alphabets are allowed as predicates. Lowercase letters are treated as variables Use of empty premises is not allowed.

• Conjunction (And Operation): The operator for conjunction is represented by the symbol "∧" or "&". It combines two propositions and is true only when both propositions are true.
  Example: P ∧ Q, A & B
• Disjunction (Or Operation): The operator for disjunction is represented by the symbol "∨" or "|". It combines two propositions and is true when at least one of the propositions is true.
  Example: P ∨ Q, A | B
• Material Implication: The operator for material implication is represented by the symbol "->. It represents "if...then..." statements and is true unless the first proposition is true and the second is false.
  Example: P -> Q
• Biconditional: The operator for biconditional is represented by the symbol "<->". It represents "if and only if" statements and is true when both propositions have the same truth value.
  Example: P <-> Q
• Negation: For the operator of negation, the symbols "~", "!", and "¬" are permissible. It is used to reverse the truth value of a proposition.
  Example: ~P, !(P -> Q), ¬R
• Universal Quantifier (∀): The symbol '∀' is used to represent the universal quantifier in First-Order Logic. It indicates that a statement holds true for all objects in a specified domain. The binding varaible must be along side the quantifier whereas the scope must be bound in parantheses.
  Example: ∀x (Px), ∀x (Px -> Qx)
• Existential Quantifier (∃): The symbol '∃' is used to represent the existential quantifier in First-Order Logic. It indicates that there exists at least one object in a specified domain for which a statement is true. The binding varaible must be along side the quantifier whereas the scope must be bound in parantheses.
  Example: ∃x (Qx), ∃x (Qx -> Px)

Supported Rules

• Modus Ponens (MP) (Also known as: Implication Elimination, Affirming the Antecedent)

  Modus Ponens is a valid rule of inference that states if you have a conditional statement (p → q) and the antecedent (p) is true, then you can infer that the consequent (q) is also true.

• Modus Tollens (MT) (Also known as: Denying the Consequent)

  Modus Tollens is a valid rule of inference that states if you have a conditional statement (p → q) and the consequent (q) is false, then you can infer that the antecedent (p) must also be false.

• Material Implication (MI) (Also known as: Implication Equivalence)

  Material Implication is a logical equivalence rule that simplifies conditional statements. It states that (p → q) is equivalent to (¬p ∨ q), where ¬ represents negation and ∨ represents disjunction.

• De Morgan's Laws

  De Morgan's Laws are a set of rules that describe how to negate conjunctions and disjunctions. They state that ¬(p ∧ q) is equivalent to (¬p ∨ ¬q) and ¬(p ∨ q) is equivalent to (¬p ∧ ¬q).

• Simplification (S) (Also known as: Conjunction Elimination)

  Simplification is a rule that allows you to simplify a conjunction (p ∧ q) to its individual components (p and q).

• Hypothetical Syllogism (HS) (Also known as: Transitive Law)

  Hypothetical Syllogism is a valid rule of inference that states if you have two conditional statements (p → q) and (q → r), you can infer the conditional statement (p → r).

• Biconditional Elimination

  Biconditional Elimination is a rule that allows you to extract the implications from a biconditional statement (p ↔ q). It results in two conditional statements: (p → q) and (q → p).

• Biconditional Introduction

  The Biconditional Introduction is a fundamental rule in propositional logic. It allows you to establish a biconditional statement (p ↔ q) when you have both implications: (p → q) and (q → p). In other words, if you have 'p implies q' and 'q implies p,' you can infer the biconditional 'p if and only if q.' This rule is used to express that two propositions are logically equivalent and can be interchanged in logical reasoning.

• Disjunctive Syllogism (DS)

  Disjunctive Syllogism is a valid rule of inference that states if you have a disjunction (p ∨ q) and the negation of one disjunct (¬p or ¬q), you can infer the other disjunct.

• Addition

  The Addition Rule is a logical inference rule that allows you to introduce a disjunction (OR) by asserting one of its disjuncts. In other words, if you have a proposition p, you can derive the statement (p ∨ q), where q represents any arbitrary proposition. This rule is useful when you want to expand your set of premises or conclusions by asserting a new possibility.

• Double Negation (DN)

  Double Negation is a rule that states that double negating a proposition (¬¬p) is equivalent to the original proposition (p).

• Conjunction

  The Conjunction Rule, also known as Simplification, is a fundamental rule of propositional logic. It states that if we have two individual propositions 'A' and 'B,' then we can infer the conjunction 'A and B' (A ∧ B). This rule allows us to simplify complex propositions by breaking them down into their constituent parts for analysis and inference.

• Transposition (Also known as: Contrapositive)

  The Transposition Rule, also known as the Contrapositive, is a fundamental rule in propositional logic. It allows us to transform an implication (p → q) into its contrapositive form (¬q → ¬p). In other words, if we have an implication 'p implies q,' we can infer its contrapositive, which states that 'not q implies not p.'

• Negation (¬)

  Negation, often denoted as ¬, is a fundamental logical operation that negates a proposition. If a proposition p is true, then ¬p is false, and if p is false, then ¬p is true.

• Existential Generalization (EG) (Also known as: existential introduction)

  Existential Generalization, often denoted as EG, is a valid rule of inference in predicate logic. It allows you to infer the existence of an element that satisfies a predicate.

• Universal Generalization (UG) (Also known as: universal introduction)

  Universal Generalization, often denoted as UG, is a valid rule of inference used in predicate logic. It allows you to generalize a statement from a specific instance to all elements of a set.

• Existential Instantiation (EI) (Also known as: existential elimination)

  Existential Instantiation, often denoted as EI, is a valid rule of inference in predicate logic. It allows you to instantiate an existential quantifier (∃) with a specific element that satisfies the existential statement.

• Universal Instantiation (UI) (Also known as: universal specification, universal elimination)

  Universal Instantiation, often denoted as UI, is a valid rule of inference in predicate logic. It allows you to instantiate a universal quantifier (∀) with a specific element from a set.