Propose

Propose is a playground for creating, manipulating, and verifying statements in propositional logic.

It comes with a simple command-line REPL propose, which can answer questions about propositional statements.

• Requirements
• Installation
• Writing Formulas
• Commands
• License

Ruby 2.4+

gem install propose

You can write formulas with Propose in plain English (e.g. p or q), or use the standard propositional calculus notation (e.g. p ∨ q), amongst a few other options outlined below.

Atoms are the basic unit of propositional logic, and represent a single statement which can be true or false, like "The sun is shining." They can be written in one or more lowercase letters.

> p
> q
> ball

The negation of an atom expresses that the statement is not true. Negation can also be applied to larger expressions.

> not p
> ¬p
> !p

The conjunction of two expressions denotes that both expressions are true.

> p and q
> p ∧ q
> p & q

The disjunction of two expressions denotes that at least one of the expressions is true.

> p or q
> p ∨ q
> p | q

Implication expresses the concept that the expression on the right is a logical consequence of the expression on the left, e.g. "if the sun is shining, then the ice is melting".

> p implies q
> p imply q
> p → q
> p -> q
> p => q

You can write arbitrarily complex formulas by using parentheses to nest expressions.

> p or (q and r)
> (p or q) implies (q or r)
> not (p and q)

For convenience, you can avoid writing unnecessary parentheses by adhering to the conventions below:

• ¬ binds more tightly than ∧, meaning ¬p ∧ q denotes (¬p) ∧ q
• ∧ binds more tightly than ∨, meaning p ∧ q ∨ r denotes (p ∧ q) ∨ r
• ∨ binds more tightly than →, meaning p ∨ q → q ∨ r denotes (p ∨ q) → (q ∨ r)
• → is right-associative, meaning p → q → r denotes p → (q → r)

To print out a truth table for a propositional formula, simply enter the formula as a command.

> not p or q and r
+---+---+---+--------+
|    ¬p ∨ (q ∧ r)    |
+---+---+---+--------+
| p | q | r | Result |
+---+---+---+--------+
| T | T | T |   T    |
| F | T | T |   T    |
| T | F | T |   F    |
| F | F | T |   T    |
| T | T | F |   F    |
| F | T | F |   T    |
| T | F | F |   F    |
| F | F | F |   T    |
+---+---+---+--------+

This project is released under the MIT license.