Skip to content

Instantly share code, notes, and snippets.

@fhightower
Last active January 14, 2020 02:09
Show Gist options
  • Save fhightower/d9cc7e7e2c7dc4898edf52695c117a14 to your computer and use it in GitHub Desktop.
Save fhightower/d9cc7e7e2c7dc4898edf52695c117a14 to your computer and use it in GitHub Desktop.
Validation of the logic behind affirmations on the Roman Catholic Church's and Luther's teaching on baptism
/* You can test this code here: https://swish.swi-prolog.org/example/examples.swinb */
x('Baptism is necessary for salvation in most cases').
teaches(rcc, x).
teaches(luther, x).
false(x).
falseTeacher(N) :- teaches(N, X), false(X).
/* ?- falseTeacher(luther). (returns: true) */
/* ?- falseTeacher(rcc). (returns: true) */
from z3 import *
# I'm using the abbreviation `rcc` to refer to the Roman Catholic Church
# represent the rcc and luther's teaching on baptism as a boolean value (true or false)
rcc_baptism_teaching = Bool('rcc_baptism_teaching')
luther_baptism_teaching = rcc_baptism_teaching
# for the sake of argument, assume that the rcc's teaching on baptism is not true (as claimed here: https://immanuelbible.church/content/catholic)
axioms = [
Not(rcc_baptism_teaching)
]
# create a z3 solver (see more here: http://theory.stanford.edu/~nikolaj/programmingz3.html)
s = Solver()
# we add our axioms
s.add(axioms)
# we assert that luther's teaching on baptism is not true
s.add(Not(luther_baptism_teaching))
# this prints "sat" meaning that the logic is satisfiable (see more here: https://en.wikipedia.org/wiki/Satisfiability) meaning the logic is valid
print(s.check())
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment