Many-Valued Logic Explorer Generator

Install Python on https://www.python.org
To install PIP, follow instructions from https://pip.pypa.io/
To install Z3, follow instructions from https://pypi.org/project/z3-solver/
(Source code here • Some basic (sub)structurality here)

Presentation

Have a proof calculus and want to show it's non-trivial? Or variable sharing? Or non-symmetric implication? Or basically anything of the form Γ⊬p (existentially or universally)? Sounds like you need a sound (finitely) many-valued model! If one exists, this tool will find it. Guaranteed 100% without LLM hallucination (it uses the Z3 SAT solver, and most importantly, not an ounce of AI). Even this page's HTML, PHP and Python codes are made with my ~~paws~~ hands all the way through (well, given how garbage it is, it better be).

Metasyntax

Encoding	Name	Arity
Entails	Entailment (⊢)	Binary (relation)
Comma	Comma (,)	Binary
Not	"Not ..."	Unary
Implies	"If... then..."	Binary
And	"... and ..."	Any arity
Or	"... and/or ..."	Any arity

Syntax

Encoding	Name	Arity
N	Negation (~)	Unary
C	Implication (→)	Binary
K	Conjunction (&)	Binary
A	Disjunction (∨)	Binary

Rules

from z3 import *
from itertools import product
from time import time

found = False
size = 1

while not found :
    
    start = time()
    
    V = list(range(size))
    inV = lambda x : And(x >= 0, x < size)
    
    Entails = Function("Entails", IntSort(), IntSort(), BoolSort())
    Neutral = Int("Neutral")
    Comma = Function("Comma", IntSort(), IntSort(), IntSort())
    C = Function("C", IntSort(), IntSort(), IntSort())
    N = Function("N", IntSort(), IntSort())
    K = Function("K", IntSort(), IntSort(), IntSort())
    A = Function("A", IntSort(), IntSort(), IntSort())
        
    s = Solver()
    
    # Stability
    s.add(inV(Neutral))
    s.add(And([
        inV(N(p))
        for p in V
    ]))
    s.add(And([
        And (
            inV(Comma(p,q)),
            inV(C(p,q)),
            inV(K(p,q)),
            inV(A(p,q))
        )
        for p, q in product(*([V]*2))
    ]))
    
    # For ordering's sake
    
    s.add(And([ # Undesignated values before designated ones
            Implies(
                And(
                    Not(Entails(Neutral, a)),
                    Entails(Neutral, b)
                ),
                a < b
            )
            for a, b in product(*([V]*2))
        ]))
    s.add(And([ # Gaps after "false" values
            Implies(
                And(
                    Entails(Neutral, N(a)),
                    Not(Entails(Neutral, N(b))),
                    Entails(Neutral, a),
                    Entails(Neutral, b),
                ),
                a < b
            )
            for a, b in product(*([V]*2))
        ]))
    s.add(And([ # Gluts before "true" values
            Implies(
                And(
                    Entails(Neutral, N(a)),
                    Not(Entails(Neutral, N(b))),
                    Not(Entails(Neutral, a)),
                    Not(Entails(Neutral, b)),
                ),
                a < b
            )
            for a, b in product(*([V]*2))
        ]))
    s.add(And([ # Boths and Neithers in the middle :3
            Implies(
                And(
                    a == N(a),
                    b != N(b),
                    Entails(Neutral,a) == Entails(Neutral,b)
                ),
                And(
                    Implies(
                        Not(Entails(Neutral,a)),
                        b <= a
                    ),
                    Implies(
                        Entails(Neutral,a),
                        a <= b
                    )
                )
            )
            for a, b in product(*([V]*2))
        ]))
    s.add(And([ # Neutral = inf(V^+) under integer ordering
            Implies(
                Entails(Neutral, a),
                Neutral <= a
            )
            for a in V
        ]))
    
    # Rules
    
        
    # Solving and display
    
    print(f"Solving at size {size}...")
    
    if s.check() == sat :
        
        end = time()
        
        print(f"SAT at size {size}")
        print(f"Solved in {end-start} seconds")
        m = s.model()
    
        print("\ninf(V^+) under integer ordering: ", m.eval(Neutral))
    
        print("\nEntailment:")
        print('⊢','|',*[a for a in V],sep='\t')
        print('----','+---',*['----' for a in V],sep='\t')
        for a in V :
            print(a,'|',*[m.eval(Entails(a,b)) for b in V],sep="\t")
    
        print("\nComma:")
        print(',','|',*[a for a in V],sep='\t')
        print('----','+---',*['----' for a in V],sep='\t')
        for a in V :
            print(a,'|',*[m.eval(Comma(a,b)) for b in V],sep="\t")
        
        print("\nNegation:")
        for a in V :
            print(f"~{a}",'|',m.eval(N(a)),sep="\t")
        
        print("\nImplication:")
        print('→','|',*[a for a in V],sep='\t')
        print('----','+---',*['----' for a in V],sep='\t')
        for a in V :
            print(a,'|',*[m.eval(C(a,b)) for b in V],sep="\t")
        
        print("\nConjunction:")
        print('&','|',*[a for a in V],sep='\t')
        print('----','+---',*['----' for a in V],sep='\t')
        for a in V :
            print(a,'|',*[m.eval(K(a,b)) for b in V],sep="\t")
        
        print("\nDisjunction:")
        print('∨','|',*[a for a in V],sep='\t')
        print('----','+---',*['----' for a in V],sep='\t')
        for a in V :
            print(a,'|',*[m.eval(A(a,b)) for b in V],sep="\t")
                
        print("\nMVLPG link")
        
        print(f"https://alexandrae.fr/mvlpg.php?n={size}", end='')
        for i in range(size) :
            if m.eval(Entails(Neutral, i)) :
                print(f"&v{i}={i}&d{i}=y",end='')
            else :
                print(f"&v{i}={i}&d{i}=n",end='')
        
        for a in V :
            print(f"&N{a}=", m.eval(N(a)), sep='', end='')
        
        for a in V :
            for b in V :
                print(f"&K{a};{b}=", m.eval(K(a,b)), sep='', end='')
    
        for a in V :
            for b in V :
                print(f"&A{a};{b}=", m.eval(A(a,b)), sep='', end='')
    
        for a in V :
            for b in V :
                print(f"&C{a};{b}=", m.eval(C(a,b)), sep='', end='')
    
        found = True
    
    else :
        
        end = time()
        
        print(f"UNSAT at size {size}")
        print(f"Solved in {end-start} seconds\n")
        
        size += 1