c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%read "../../propositional/soundness/modules.elf".
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundForall : ForallPF -> ForallMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBaseFOL.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include ForallMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder forallI := [F][p : {x} ded (F x) eq 1] forall1' (forallI [x] (p x)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder forallE := [F][p : ded (forall'' [x] F x) eq 1] [c]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (indirect ([q : ded (F c) eq 0] contra (forall0' (existsI c q)) p)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundExists : ExistsPF -> ExistsMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBaseFOL.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include ExistsMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder existsI := [F][x][p : ded (F x) eq 1] exists1' (existsI x p).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder existsE := [F][G][p : ded (exists'' [x] F x) eq 1]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder [f : {y} ded (F y) eq 1 -> ded G eq 1]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (indirect ([q : ded G eq 0]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder contra (exists0' (forallI [y] indirect' ([r : ded F y eq 1] contra q (f y r))))
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder%view SoundEqual : EqualPF -> EqualMOD = {
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include SoundBaseFOL.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %include EqualMODView.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder %% alternatively use equal1 instead of (equivEl equaliff)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder refl := [X] equivEl equaliff refl.
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder sym := [X: elem univ][Y: elem univ][p : ded (X eq'' Y) eq 1]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder equivEl equaliff (sym (equivEr equaliff p)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder trans := [X][Y][Z][p : ded (X eq'' Y) eq 1][q : ded (Y eq'' Z) eq 1]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder equivEl equaliff (trans (equivEr equaliff p)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (equivEr equaliff q)).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder congF := [X][Y][p : ded (X eq'' Y) eq 1][F : elem univ -> elem univ]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder equivEl equaliff (congF (equivEr equaliff p) F).
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder congP := [X][Y][p : ded (X eq'' Y) eq 1][F][q : ded (F X) eq 1]
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder (congP (equivEr equaliff p)
c6506aa7090643badb5a6dca5df0ca6617558f5eChristian Maeder ([a] (F a) eq 1)