%% PVS Version 4.2 - Allegro CL Enterprise Edition 8.1 [Linux (x86)] (Jul 20, 2008 2:00) %% 8.1 [Linux (x86)] (Jul 20, 2008 2:00) $$$ontological.pvs ontological: THEORY BEGIN beings: TYPE x, y: VAR beings >: (trichotomous?[beings]) greatest: setof[beings] = {x| NOT EXISTS y: y>x} P1: AXIOM nonempty?(greatest) P1a: LEMMA singleton?(greatest) really_exists(x): bool someone: AXIOM EXISTS x: really_exists(x) reality_trumps: AXIOM (really_exists(x) AND NOT really_exists(y)) => x>y God_exists: THEOREM really_exists(the(greatest)) % Circularity of Zalta and Oppenheimer's P2 % Can prove this from the conclusion % Can also prove it from our axioms P2: COROLLARY (NOT really_exists(the(greatest))) => EXISTS y: (y > the(greatest)) END ontological interpretation: THEORY BEGIN IMPORTING ontological{{ beings := nat, > := <, really_exists := LAMBDA (x: nat): x<4}} AS model END interpretation $$$ontological.prf (ontological (greaterp_TCC1 0 (greaterp_TCC1-1 nil 3580569646 3586789595 ("" (inst + "lambda (x,y:beings): true") (("" (expand "trichotomous?") (("" (propax) nil nil)) nil)) nil) proved-complete ((TRUE const-decl "bool" booleans nil) (trichotomous? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (beings type-decl nil ontological nil)) 8 0 t nil)) (P1a 0 (shorter "shorter" 3580668752 3587925324 ("" (use "P1") (("" (grind :if-match nil) (("" (inst 2 "x!1") (("" (typepred ">") (("" (lazy-grind :if-match all) nil nil)) nil)) nil)) nil)) nil) proved ((greatest const-decl "setof[beings]" ontological nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (singleton? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (beings type-decl nil ontological nil) (pred type-eq-decl nil defined_types nil) (trichotomous? const-decl "bool" orders nil) (> const-decl "(trichotomous?[beings])" ontological nil) (x!1 skolem-const-decl "beings" ontological nil) (P1 formula-decl nil ontological nil)) 4975 80 t shostak) (P1a-1 nil 3580575589 3580577217 ("" (expand "singleton?") (("" (use "P1") (("" (expand "nonempty?") (("" (expand "empty?") (("" (skolem-typepred) (("" (expand "member") (("" (inst + "x!1") (("" (skolem-typepred) (("" (expand "greatest") (("" (inst 1 "x!1") (("" (inst + "y!1") (("" (typepred ">") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((greatest const-decl "setof[beings]" ontological nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (singleton? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (beings type-decl nil ontological nil) (pred type-eq-decl nil defined_types nil) (trichotomous? const-decl "bool" orders nil) (> const-decl "(trichotomous?[beings])" ontological nil) (P1 formula-decl nil ontological nil)) 69 20 t shostak)) (God_exists_TCC1 0 (God_exists_TCC1-1 nil 3587925267 3587926127 ("" (use "P1a") nil nil) proved ((P1a formula-decl nil ontological nil)) 209438 10 t nil)) (God_exists 0 (God_exists-2 "uses trumps2" 3586792875 3587925770 ("" (lemma "someone") (("" (skosimp) (("" (typepred "the(greatest)") (("" (expand "greatest" -1 1) (("" (lemma "reality_trumps") (("" (inst?) (("" (ground) (("" (inst? +) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((reality_trumps formula-decl nil ontological nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (beings type-decl nil ontological nil) (setof type-eq-decl nil defined_types nil) (greatest const-decl "setof[beings]" ontological nil) (set type-eq-decl nil sets nil) (singleton? const-decl "bool" sets nil) (the const-decl "(p)" sets nil) (someone formula-decl nil ontological nil)) 8140 50 t shostak) (God_exists-1 nil 3580575897 3586792767 ("" (lemma "reality_trumps") (("" (inst - _ "the(greatest)") (("" (ground) (("" (use "someone") (("" (skosimp) (("" (inst - "x!1") (("" (ground) (("" (typepred "the(greatest)") (("" (expand "greatest" -1 1) (("" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((beings type-decl nil ontological nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (singleton? const-decl "bool" sets nil) (the const-decl "(p)" sets nil) (setof type-eq-decl nil defined_types nil) (greatest const-decl "setof[beings]" ontological nil) (NOT const-decl "[bool -> bool]" booleans nil) nil) 89566 10 t shostak)) (P2 0 (P2-2 "proof from our lemmas" 3587925889 3587925889 ("" (ground) (("" (lemma "someone") (("" (skosimp) (("" (inst?) (("" (typepred "the(greatest)") (("" (expand "greatest" -1 1) (("" (lemma "reality_trumps") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved nil 93055 20 t shostak) (P2-1 nil 3586787800 3587925789 ("" (skosimp) (("" (use "God_exists") nil nil)) nil) proved ((someone formula-decl nil ontological nil) (beings type-decl nil ontological nil) (reality_trumps formula-decl nil ontological nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (greatest const-decl "setof[beings]" ontological nil) (set type-eq-decl nil sets nil) (singleton? const-decl "bool" sets nil) (the const-decl "(p)" sets nil)) 4773 0 t shostak))) (interpretation (model_P1_TCC1 0 (model_P1_TCC1-1 nil 3580658083 3586789595 ("" (expand "greatest") (("" (grind :if-match nil) (("" (inst - "0") (("" (grind) nil nil)) nil)) nil)) nil) proved-complete ((strict_total_order_restrict application-judgement "(strict_total_order?[S])" restrict_order_props nil) (trichotomous_restrict application-judgement "(trichotomous?[S])" restrict_order_props nil) (strict_order_restrict application-judgement "(strict_order?[S])" restrict_order_props nil) (transitive_restrict application-judgement "(transitive?[S])" restrict_order_props nil) (antisymmetric_restrict application-judgement "(antisymmetric?[S])" restrict_order_props nil) (irreflexive_restrict application-judgement "(irreflexive?[S])" restrict_order_props nil) (nonempty? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (greatest const-decl "setof[beings]" ontological nil)) 178 130 t nil)) (model_someone_TCC1 0 (model_someone_TCC1-1 nil 3580658083 3586789595 ("" (inst + "2") (("" (assert) nil nil)) nil) proved-complete ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) 6 0 t nil)) (model_reality_trumps_TCC1 0 (model_reality_trumps_TCC1-1 nil 3580658083 3586789595 ("" (mapped-axiom-tcc) nil nil) proved-complete ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) 35 20 t nil)))