c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundTruth : TruthPF -> TruthMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBase.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include TruthMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder trueI := true1.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundFalsity : FalsityPF -> FalsityMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBase.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include FalsityMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder falseE := [p : ded false' eq 1][A]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (falseE' (contra false0 p)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundIMP : IMPPF -> IMPMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBase.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include IMPMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder impI := [A][B][p: ded A eq 1 -> ded B eq 1] (
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (orE (boole A)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([q : ded A eq 1] orIr (p q))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([q : ded A eq 0] orIl q)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder impE := [A][B][p : ded (A imp'' B) eq 1][q : ded A eq 1] (
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orE (boole B)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([r : ded B eq 1] r)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([r : ded B eq 0] falseE' (contra (imp0' (andI q r)) p))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundNEG : NEGPF -> NEGMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBase.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include NEGMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder notI := [A][p : ded A eq 1 -> {B} ded B eq 1] (
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orE (boole A)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([q : ded A eq 1] p q (not'' A))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([q : ded A eq 0] not1' q)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder notE := [A] ([q : ded (not'' A) eq 1] [p : ded A eq 1] [B] falseE' (contra (not0' p) q)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundCONJ : CONJPF -> CONJMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBase.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include CONJMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder andI := [A][B][p : ded A eq 1] [q : ded B eq 1] (
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder and1' (andI p q)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder andEl := [A][B][p : ded (A and'' B) eq 1] (
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder indirect [q : ded A eq 0]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (contra (and0' (orIl q)) p)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder andEr := [A][B][p : ded (A and'' B) eq 1] (
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder indirect [q : ded B eq 0]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (contra (and0' (orIr q)) p)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundDISJ : DISJPF -> DISJMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBase.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include DISJMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orIl := [A][B][p : ded A eq 1] (or1' (orIl p)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orIr := [B][A][p : ded B eq 1] or1' (orIr p).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orE := [A][B][C][p : ded (A or'' B) eq 1] [q : ded A eq 1 -> ded C eq 1][r : ded B eq 1 -> ded C eq 1] (
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder orE (boole A)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([s : ded A eq 1] q s)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([s : ded A eq 0] orE (boole B)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([t : ded B eq 1] r t)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([t : ded B eq 0] falseE' (contra
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (or0' (andI s t))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundTND : TND -> PLMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBase.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include NEGMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include DISJMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder tnd := [A] (orE (boole A)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([p : ded A eq 1] or1' (orIl p))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([p : ded A eq 0] or1' (orIr (not1' p)))