An easy-to-use utility for propositional logic written in vanilla Python.
Let's admit it, anyone would find equivalency/validity tests with truth tables tedious, especially when it comes to something like this:
(okay for those of who don't think this is a hard proof, you guys rock)
I grew weary of doing long-winded truth tables to verify if I had done a proof right, so I decided to write a tool that does the dirty work for me.
I use it occasionally to check if my "logic" is right, and I think it may benefit many propositional logic learners out there!
Scenarios:
- You drew a truth table and wanted to see if you did it right.
- You're done with quite a long proof and you want to see if your steps are right.
- You need to show someone some "logic." (tutoring maybe?)
- You need to check if your argument is valid before embarrassing yourself in front of your geeky friends. (this one's a bit far-fetched)
You're too lazy to do your homework and you...(uh no no)- And more... Really, you're only limited by your imagination...
- Draw and/or export a truth table w/wo constituent sentences.
- Logical equivalency test for multiple propositional statements.
- Validity test for logical arguments.
- Light-weighted and no dependencies needed.
- Fast and beautiful (okay-looking) output format.
- More features are coming...
Windows-friendly.
Here I'm only showing Homebrew (but really, you can get it from anywhere, as long as it's legit):
brew install python3
Download the source code and decompress it.
You're all set! No dependencies whatsoever!
Feel free to do this and get started:
cd /source/code/root
python3 ./logic.py [...] # do this instead of ./logic-util
Sorry Windows users, you'll need the source code (for now). 😢
Download the latest binary from releases.
You may need to change the file mode of logic-util
to use it:
cd /root/of/binary
chmod +x ./logic-util
You're all set! No dependencies, not even Python!
- macOS
OR - Python 3.8+
Operators | |
---|---|
Negation | not NOT ~ ∼ ¬ ! |
(Inclusive) Disjunction | or OR ∨ | + |
Conjunction | and AND ∧ & * ⋅ |
Implication | to -> → ⟹ ⟶ ⇒ |
Bicondition | iff IFF <-> ↔ ⇔ ⟷ ⟺ |
Exclusive Disjunction | xor XOR ⊻ ⊕ ⨁ ^ |
(from high to low)
- Parentheses:
()
- Negation (NOT)
- Conjunction (AND)
- (Inclusive) Disjunction (OR)
- Exclusive Disjunction (XOR)
- Implication (→)
- Bicondition (↔︎)
The standard way of making a truth table for a proposition logic statement:
> ./logic-util make-table '(a or b) -> c'
┏━━━┯━━━┯━━━┯━━━━━━━┯━━━━━━━━━━━━━┓
┃ a │ b │ c │ a ∨ b │ (a ∨ b) → c ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 0 │ 0 │ 0 │ 0 │ 1 ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 0 │ 0 │ 1 │ 0 │ 1 ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 0 │ 1 │ 0 │ 1 │ 0 ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 0 │ 1 │ 1 │ 1 │ 1 ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 1 │ 0 │ 0 │ 1 │ 0 ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 1 │ 0 │ 1 │ 1 │ 1 ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 1 │ 1 │ 0 │ 1 │ 0 ┃
┠───┼───┼───┼───────┼─────────────┨
┃ 1 │ 1 │ 1 │ 1 │ 1 ┃
┗━━━┷━━━┷━━━┷━━━━━━━┷━━━━━━━━━━━━━┛
Note
Your statement should be wrapped in a pair of quotation marks''
or""
.
The rightmost column is the output column of the propositional statement
By default, the truth table is drawn with columns for all the constituent atomic sentences (-n
or --no-atoms
. Now, only the output column will be drawn:
> ./logic-util make-table '(a or b) -> c' -n
┏━━━┯━━━┯━━━┯━━━━━━━━━━━━━┓
┃ a │ b │ c │ (a ∨ b) → c ┃
┠───┼───┼───┼─────────────┨
┃ 0 │ 0 │ 0 │ 1 ┃
┠───┼───┼───┼─────────────┨
┃ 0 │ 0 │ 1 │ 1 ┃
┠───┼───┼───┼─────────────┨
┃ 0 │ 1 │ 0 │ 0 ┃
┠───┼───┼───┼─────────────┨
┃ 0 │ 1 │ 1 │ 1 ┃
┠───┼───┼───┼─────────────┨
┃ 1 │ 0 │ 0 │ 0 ┃
┠───┼───┼───┼─────────────┨
┃ 1 │ 0 │ 1 │ 1 ┃
┠───┼───┼───┼─────────────┨
┃ 1 │ 1 │ 0 │ 0 ┃
┠───┼───┼───┼─────────────┨
┃ 1 │ 1 │ 1 │ 1 ┃
┗━━━┷━━━┷━━━┷━━━━━━━━━━━━━┛
To use custom labels for truth values (e.g. F/T instead of 0/1), use the flag -l
or --labels
with an argument specifying the custom labels as such:
> ./logic-util make-table '(a or b) -> c' -l FT
┏━━━┯━━━┯━━━┯━━━━━━━┯━━━━━━━━━━━━━┓
┃ a │ b │ c │ a ∨ b │ (a ∨ b) → c ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ F │ F │ F │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ F │ T │ F │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ T │ F │ T │ F ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ T │ T │ T │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ F │ F │ T │ F ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ F │ T │ T │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ T │ F │ T │ F ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ T │ T │ T │ T ┃
┗━━━┷━━━┷━━━┷━━━━━━━┷━━━━━━━━━━━━━┛
The argument is a two-character string in the format [FALSE_LABEL][TRUE_LABEL]
.
To reverse the truth values (e.g. from TTT
to FFF
instead of FFF
to TTT
, like the convention for truth tables in this book1), use the flag -r
or --reverse
:
> ./logic-util make-table '(a or b) -> c' -l FT -r
┏━━━┯━━━┯━━━┯━━━━━━━┯━━━━━━━━━━━━━┓
┃ a │ b │ c │ a ∨ b │ (a ∨ b) → c ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ T │ T │ T │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ T │ F │ T │ F ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ F │ T │ T │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ T │ F │ F │ T │ F ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ T │ T │ T │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ T │ F │ T │ F ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ F │ T │ F │ T ┃
┠───┼───┼───┼───────┼─────────────┨
┃ F │ F │ F │ F │ T ┃
┗━━━┷━━━┷━━━┷━━━━━━━┷━━━━━━━━━━━━━┛
Finally, to export the truth table to a .csv
file, use the flag -o
or --output
with an argument specifying the location:
> ./logic-util make-table '(a or b) -> c' -o ~/Desktop/output.csv
Specifying a file extension is optional, the utility automatically handles it for you! If no file name is provided, it will be saved at the specified location as output.csv
by default.
Alternatively, if no statement is provided as an argument to make-table
, the utility will enter interactive mode with the given options.
> ./logic-util make-table [OPTIONS]
Enter a statement: ▊
Enter a propositional statement to make a truth table out of it. You can do this as many time as you want.
To exit, hit Ctrl + C, Ctrl + D, or return without any input.
Example scenario: Export multiple truth tables efficiently.
> ./logic-util make-table -l FT -o ~/Desktop/output
Enter a statement: (a or b) -> c
Enter a statement: (a and b) -> c
Enter a statement: (a iff b) or c
Enter a statement: ▊
The truth tables will be saved directly to your specified location (they won't be printed in Terminal), you'll now see output.csv
, output-1.csv
, and output-2.csv
with respective truth tables at ~/Desktop
.
To test if two propositional logic statements are logically equivalent, use the check-equivalence
keyword:
> ./logic-util check-equivalence '~(a or b)' '~a and ~b'
1. ¬(a ∨ b)
2. ¬a ∧ ¬b
┏━━━┯━━━┯━━━━━━━━━━┯━━━━━━━━━┯━━━┓
┃ a │ b │ ¬(a ∨ b) │ ¬a ∧ ¬b │ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 0 │ 0 │ 1 │ 1 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 0 │ 1 │ 0 │ 0 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 1 │ 0 │ 0 │ 0 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 1 │ 1 │ 0 │ 0 │ ✓ ┃
┗━━━┷━━━┷━━━━━━━━━━┷━━━━━━━━━┷━━━┛
✓ The statements are logically equivalent!
Or even multiple statements:
> ./logic-util check-equivalence '~(a or b)' '~a and ~b' '~(~a -> b)' '~(a and (a or b) or b)'
1. ¬(a ∨ b)
2. ¬a ∧ ¬b
3. ¬(¬a → b)
4. ¬((a ∧ (a ∨ b)) ∨ b)
┏━━━┯━━━┯━━━━━━━━━━┯━━━━━━━━━┯━━━━━━━━━━━┯━━━━━━━━━━━━━━━━━━━━━━┯━━━┓
┃ a │ b │ ¬(a ∨ b) │ ¬a ∧ ¬b │ ¬(¬a → b) │ ¬((a ∧ (a ∨ b)) ∨ b) │ ┃
┠───┼───┼──────────┼─────────┼───────────┼──────────────────────┼───┨
┃ 0 │ 0 │ 1 │ 1 │ 1 │ 1 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───────────┼──────────────────────┼───┨
┃ 0 │ 1 │ 0 │ 0 │ 0 │ 0 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───────────┼──────────────────────┼───┨
┃ 1 │ 0 │ 0 │ 0 │ 0 │ 0 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───────────┼──────────────────────┼───┨
┃ 1 │ 1 │ 0 │ 0 │ 0 │ 0 │ ✓ ┃
┗━━━┷━━━┷━━━━━━━━━━┷━━━━━━━━━┷━━━━━━━━━━━┷━━━━━━━━━━━━━━━━━━━━━━┷━━━┛
✓ The statements are logically equivalent!
If you wish to see truth table for each test combination, set the mode using the flag -m
or --mode
to paired
:
> ./logic-util check-equivalence '~(a or b)' '~a and ~b' '~(a -> b)' -m paired
1. ¬(a ∨ b)
2. ¬a ∧ ¬b
3. ¬(a → b)
Test 1: ¬(a ∨ b) ≡ ¬a ∧ ¬b
┏━━━┯━━━┯━━━━━━━━━━┯━━━━━━━━━┯━━━┓
┃ a │ b │ ¬(a ∨ b) │ ¬a ∧ ¬b │ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 0 │ 0 │ 1 │ 1 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 0 │ 1 │ 0 │ 0 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 1 │ 0 │ 0 │ 0 │ ✓ ┃
┠───┼───┼──────────┼─────────┼───┨
┃ 1 │ 1 │ 0 │ 0 │ ✓ ┃
┗━━━┷━━━┷━━━━━━━━━━┷━━━━━━━━━┷━━━┛
Test 2: ¬(a ∨ b) ≡ ¬(a → b)
┏━━━┯━━━┯━━━━━━━━━━┯━━━━━━━━━━┯━━━┓
┃ a │ b │ ¬(a ∨ b) │ ¬(a → b) │ ┃
┠───┼───┼──────────┼──────────┼───┨
┃ 0 │ 0 │ 1 │ 0 │ ✗ ┃
┠───┼───┼──────────┼──────────┼───┨
┃ 0 │ 1 │ 0 │ 0 │ ✓ ┃
┠───┼───┼──────────┼──────────┼───┨
┃ 1 │ 0 │ 0 │ 1 │ ✗ ┃
┠───┼───┼──────────┼──────────┼───┨
┃ 1 │ 1 │ 0 │ 0 │ ✓ ┃
┗━━━┷━━━┷━━━━━━━━━━┷━━━━━━━━━━┷━━━┛
Test 3: ¬a ∧ ¬b ≡ ¬(a → b)
┏━━━┯━━━┯━━━━━━━━━┯━━━━━━━━━━┯━━━┓
┃ a │ b │ ¬a ∧ ¬b │ ¬(a → b) │ ┃
┠───┼───┼─────────┼──────────┼───┨
┃ 0 │ 0 │ 1 │ 0 │ ✗ ┃
┠───┼───┼─────────┼──────────┼───┨
┃ 0 │ 1 │ 0 │ 0 │ ✓ ┃
┠───┼───┼─────────┼──────────┼───┨
┃ 1 │ 0 │ 0 │ 1 │ ✗ ┃
┠───┼───┼─────────┼──────────┼───┨
┃ 1 │ 1 │ 0 │ 0 │ ✓ ┃
┗━━━┷━━━┷━━━━━━━━━┷━━━━━━━━━━┷━━━┛
Summary: 1/3 tests passed.
┏━━━━━━━━━━━━━━━━━━━┯━━━┓
┃ Tests │ ┃
┠───────────────────┼───┨
┃¬(a ∨ b) ≡ ¬a ∧ ¬b │ ✓ ┃
┠───────────────────┼───┨
┃¬(a ∨ b) ≡ ¬(a → b)│ ✗ ┃
┠───────────────────┼───┨
┃¬a ∧ ¬b ≡ ¬(a → b) │ ✗ ┃
┗━━━━━━━━━━━━━━━━━━━┷━━━┛
✗ The statements are not logically equivalent!
Additional flags -l
/--labels
, -r
/--reverse
, and -o
/--output
also apply.
Note
The flag-o
/--output
will be ignored when-m
/--mode
is set topaired
under interactive mode (no files will be exported).
Similar to make-table
, check-equivalence
also has an interactive mode, which can be used to check multiple pairs/groups of statement at a time.
> ./logic-util check-equivalence [OPTIONS]
(1) ▊
Upon entering the interactive mode, you will be prompted to enter your propositions one by one. When you are done with a group of propositions, hit return on the next prompt to end the group and begin the test.
To exit, hit Ctrl + C, Ctrl + D, or return without any input.
To check the validity of an argument, use the keyword check-validity
as such:
> ./logic-util check-validity [PREMISE]... -c/--conclusion [CONCLUSION]
The -c
/--conclusion
flag is optional, the last premise will be taken as the conclusion of the argument if one isn't provided.
Note
This checks the validity of an argument (not whether a single proposition is a logical truth), which requires at least one premise and one conclusion.
Example: Converse Error
> ./logic-util check-validity 'a -> b' 'b' -c 'a'
1. a → b
2. b
──────────
∴ a
┏━━━┯━━━┯━━━━━━━┯━━━┓
┃ a │ b │ a → b │ ┃
┠───┼───┼───────┼───┨
┃ 0 │ 0 │ 1 │ ✓ ┃
┠───┼───┼───────┼───┨
┃ 0 │ 1 │ 1 │ ✗ ┃
┠───┼───┼───────┼───┨
┃ 1 │ 0 │ 0 │ ✓ ┃
┠───┼───┼───────┼───┨
┃ 1 │ 1 │ 1 │ ✓ ┃
┗━━━┷━━━┷━━━━━━━┷━━━┛
Countermodel: a = 0, b = 1
✗ The argument is invalid!
Additional flags -l
/--labels
, -r
/--reverse
, and -o
/--output
also apply.
Like make-table
and check-equivalence
, you can check the validity of multiple arguments in the interactive mode:
> ./logic-util check-validity [OPTIONS]
Premise 1: ▊
Upon entering the interactive mode, you will be prompted to enter the premise(s) and the conclusion of your argument. If no conclusion is provided, the last premise will be used as the conclusion.
To exit, hit Ctrl + C or Ctrl + D.
- Support for tautologies (
$\top$ ) and contradictions ($\bot$ ). - A better documentation.
- A neater codebase (some ugly code in there).
- More tests.
- More helpful error messages.
- Validity test using formal proof with rules of inference.
- Validity/Equivalency test with the truth tree method (the semantic tableaux).
- First-order logic statement evaluation and validity/equivalency test (with the truth tree method).
- A Windows executable.
- Suggest features...?
- 🍴 Simply fork the code yourself and submit a pull request to improve the tool!
- 🚩 Open an issue or discussion if you have questions, suggestions, or bugs you've found.
- 📧 Hit me up at my E-mail, Facebook, or Instagram if you'd like to discuss or help with this project (or other projects), or even just chat with me or teach me about something!
Footnotes
-
Burgess, J. P., Jeffrey, R. C. (2006). Formal logic: its scope and limits. Indianapolis: Hackett Publishing Company. ↩