5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak%read "../proof_theory/modules.elf".

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak%read "../model_theory/modules.elf".

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak%read "base.elf".

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak%view SoundTruth : TruthPF -> TruthMOD = {

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include SoundBase.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include TruthMODView.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak trueI := true1.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak}.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen%view SoundFalsity : FalsityPF -> FalsityMOD = {

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen %include SoundBase.

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen %include FalsityMODView.

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen falseE := [p : ded false' eq 1][A]

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak (falseE' (contra false0 p)).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak}.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak

3f08db06526d6901aa08c110b5bc7dde6bc39905nd%view SoundIMP : IMPPF -> IMPMOD = {

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include SoundBase.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include IMPMODView.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak impI := [A][B][p: ded A eq 1 -> ded B eq 1] (

3f08db06526d6901aa08c110b5bc7dde6bc39905nd imp1'

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak (orE (boole A)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ([q : ded A eq 1] orIr (p q))

befb6758d5618c60f29b19f9a7eb75ab993511dcjim ([q : ded A eq 0] orIl q)

e1e8390280254f7f0580d701e583f670643d4f3fnilgun )

d474d8ef01ec5c2a09341cd148851ed383c3287crbowen ).

d474d8ef01ec5c2a09341cd148851ed383c3287crbowen impE := [A][B][p : ded (A imp'' B) eq 1][q : ded A eq 1] (

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak orE (boole B)

4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluem ([r : ded B eq 1] r)

4b575a6b6704b516f22d65a3ad35696d7b9ba372rpluem ([r : ded B eq 0] falseE' (contra (imp0' (andI q r)) p))

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak}.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak%view SoundNEG : NEGPF -> NEGMOD = {

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include SoundBase.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include NEGMODView.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak notI := [A][p : ded A eq 1 -> {B} ded B eq 1] (

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak orE (boole A)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ([q : ded A eq 1] p q (not'' A))

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ([q : ded A eq 0] not1' q)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak notE := [A] ([q : ded (not'' A) eq 1] [p : ded A eq 1] [B] falseE' (contra (not0' p) q)).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak}.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak%view SoundCONJ : CONJPF -> CONJMOD = {

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include SoundBase.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include CONJMODView.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak andI := [A][B][p : ded A eq 1] [q : ded B eq 1] (

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak and1' (andI p q)).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak andEl := [A][B][p : ded (A and'' B) eq 1] (

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak indirect [q : ded A eq 0]

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak (contra (and0' (orIl q)) p)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak andEr := [A][B][p : ded (A and'' B) eq 1] (

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak indirect [q : ded B eq 0]

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak (contra (and0' (orIr q)) p)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak}.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak%view SoundDISJ : DISJPF -> DISJMOD = {

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include SoundBase.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include DISJMODView.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak orIl := [A][B][p : ded A eq 1] (or1' (orIl p)).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak orIr := [B][A][p : ded B eq 1] or1' (orIr p).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak 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] (

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak orE (boole A)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ([s : ded A eq 1] q s)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ([s : ded A eq 0] orE (boole B)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ([t : ded B eq 1] r t)

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ([t : ded B eq 0] falseE' (contra

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak (or0' (andI s t))

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak p

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak )

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak )

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak )

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak ).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak}.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak

befb6758d5618c60f29b19f9a7eb75ab993511dcjim%read "../model_theory/prop.elf".

e1e8390280254f7f0580d701e583f670643d4f3fnilgun

d474d8ef01ec5c2a09341cd148851ed383c3287crbowen%view SoundTND : TND -> PLMOD = {

d474d8ef01ec5c2a09341cd148851ed383c3287crbowen %include SoundBase.

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak %include NEGMODView.

5effc8b39fae5cd169d17f342bfc265705840014rbowen %include DISJMODView.

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd tnd := [A] (orE (boole A)

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd ([p : ded A eq 1] or1' (orIl p))

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd ([p : ded A eq 0] or1' (orIr (not1' p)))

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd ).

5652dbe450e4fcfdf36d4cfb42d7f2345ded29a4maczniak}.