Validation of the logic behind affirmations on the Roman Catholic Church's and Luther's teaching on baptism

rcc_and_luther_baptism_logic_validator.pl

/* 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) */

rcc_and_luther_baptism_logic_validator.py

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())