Counter Model Generator info

Counter-model generation via truth-functional expansion is a method used to determine whether an argument is invalid by systematically testing all possible truth values of its propositions. Unlike direct natural deduction, this approach involves breaking down complex logical statements into simpler components and evaluating their truth values under different interpretations. By expanding logical expressions and exploring all truth-functional possibilities, the counter-model generator can identify cases where the premises are true, but the conclusion is false, thereby demonstrating invalidity in an argument.

For more detailed information, see Wikipedia

See Counter Model Generator here

Input Syntax

All uppercase alphabets are allowed as predicates. Lowercase letters are treated as variables. Use of empty premises is not allowed. Uppercase letters followed by uppercase letters, e.g., A in FA, are treated as name letters.

• 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

• Universal Quantifier Expansion (∀)

  ∀x P(x) is true if and only if P(x) is true for every possible value of x in the domain. For truth-functional expansion: Expand the statement to include all instances of the domain.

• Existential Quantifier Expansion (∃)

  ∃x P(x) is true if and only if P(x) is true for at least one value of x in the domain. For truth-functional expansion: Expand the statement to include at least one instance where the predicate holds true for a value in the domain.