(*<*) theory TAO_98_ArtificialTheorems imports TAO_7_Axioms begin (*>*) section‹Artificial Theorems› text‹\label{TAO_ArtificialTheorems}› text‹ \begin{remark} Some examples of theorems that can be derived from the model structure, but which are not derivable from the deductive system PLM itself. \end{remark} › locale ArtificialTheorems begin lemma lambda_enc_1: "[⦇❙λx . ⦃x⇧^{P}, F⦄ ❙≡⦃x⇧^{P}, F⦄, y⇧^{P}⦈ in v]" by (auto simp: meta_defs meta_aux conn_defs forall_Π⇩_{1}_def) lemma lambda_enc_2: "[⦇❙λx . ⦃y⇧^{P}, G⦄, x⇧^{P}⦈ ❙≡⦃y⇧^{P}, G⦄ in v]" by (auto simp: meta_defs meta_aux conn_defs forall_Π⇩_{1}_def) text‹ \begin{remark} The following is \emph{not} a theorem and nitpick can find a countermodel. This is expected and important. If this were a theorem, the theory would become inconsistent. \end{remark} › lemma lambda_enc_3: "[(⦇❙λx . ⦃x⇧^{P}, F⦄, x⇧^{P}⦈ ❙→⦃x⇧^{P}, F⦄) in v]" apply (simp add: meta_defs meta_aux conn_defs forall_Π⇩_{1}_def) nitpick[user_axioms, expect=genuine] oops ― ‹countermodel by nitpick› text‹ \begin{remark} Instead the following two statements hold. \end{remark} › lemma lambda_enc_4: "[⦇(❙λx . ⦃x⇧^{P}, F⦄), x⇧^{P}⦈ in v] = (∃ y . νυ y = νυ x ∧ [⦃y⇧^{P}, F⦄ in v])" by (simp add: meta_defs meta_aux) lemma lambda_ex: "[⦇(❙λx . φ (x⇧^{P})), x⇧^{P}⦈ in v] = (∃ y . νυ y = νυ x ∧ [φ (y⇧^{P}) in v])" by (simp add: meta_defs meta_aux) text‹ \begin{remark} These statements can be translated to statements in the embedded logic. \end{remark} › lemma lambda_ex_emb: "[⦇(❙λx . φ (x⇧^{P})), x⇧^{P}⦈ ❙≡(❙∃y . (❙∀F . ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P})) in v]" proof(rule MetaSolver.EquivI) interpret MetaSolver . { assume "[⦇(❙λx . φ (x⇧^{P})), x⇧^{P}⦈ in v]" then obtain y where "νυ y = νυ x ∧ [φ (y⇧^{P}) in v]" using lambda_ex by blast moreover hence "[(❙∀F . ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) in v]" apply - apply meta_solver by (simp add: Semantics.d⇩_{κ}_proper Semantics.ex1_def) ultimately have "[❙∃y . (❙∀F . ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P}) in v]" using ExIRule ConjI by fast } moreover { assume "[❙∃y . (❙∀F . ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P}) in v]" then obtain y where y_def: "[(❙∀F . ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P}) in v]" by (rule ExERule) hence "⋀ F . [⦇F,x⇧^{P}⦈ in v] = [⦇F,y⇧^{P}⦈ in v]" apply - apply (drule ConjE) apply (drule conjunct1) apply (drule AllE) apply (drule EquivE) by simp hence "[⦇makeΠ⇩_{1}(λ u s w . νυ y = u),x⇧^{P}⦈ in v] = [⦇makeΠ⇩_{1}(λ u s w . νυ y = u),y⇧^{P}⦈ in v]" by auto hence "νυ y = νυ x" by (simp add: meta_defs meta_aux) moreover have "[φ (y⇧^{P}) in v]" using y_def ConjE by blast ultimately have "[⦇(❙λx . φ (x⇧^{P})), x⇧^{P}⦈ in v]" using lambda_ex by blast } ultimately show "[⦇❙λx. φ (x⇧^{P}),x⇧^{P}⦈ in v] = [❙∃y. (❙∀F. ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P}) in v]" by auto qed lemma lambda_enc_emb: "[⦇(❙λx . ⦃x⇧^{P}, F⦄), x⇧^{P}⦈ ❙≡(❙∃y . (❙∀F . ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&⦃y⇧^{P}, F⦄) in v]" using lambda_ex_emb by fast text‹ \begin{remark} In the case of proper maps, the generalized ‹β›-conversion reduces to classical ‹β›-conversion. \end{remark} › lemma proper_beta: assumes "IsProperInX φ" shows "[(❙∃y . (❙∀F . ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P})) ❙≡φ (x⇧^{P}) in v]" proof (rule MetaSolver.EquivI; rule) interpret MetaSolver . assume "[❙∃y. (❙∀F. ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P}) in v]" then obtain y where y_def: "[(❙∀F. ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P}) in v]" by (rule ExERule) hence "[⦇makeΠ⇩_{1}(λ u s w . νυ y = u), x⇧^{P}⦈ in v] = [⦇makeΠ⇩_{1}(λ u s w . νυ y = u), y⇧^{P}⦈ in v]" using EquivS AllE ConjE by blast hence "νυ y = νυ x" by (simp add: meta_defs meta_aux) thus "[φ (x⇧^{P}) in v]" using y_def[THEN ConjE[THEN conjunct2]] assms IsProperInX.rep_eq valid_in.rep_eq by blast next interpret MetaSolver . assume "[φ (x⇧^{P}) in v]" moreover have "[❙∀F. ⦇F,x⇧^{P}⦈ ❙≡⦇F,x⇧^{P}⦈ in v]" apply meta_solver by blast ultimately show "[❙∃y. (❙∀F. ⦇F,x⇧^{P}⦈ ❙≡⦇F,y⇧^{P}⦈) ❙&φ (y⇧^{P}) in v]" by (meson ConjI ExI) qed text‹ \begin{remark} The following theorem is a consequence of the constructed Aczel-model, but not part of PLM. Separate research on possible modifications of the embedding suggest that this artificial theorem can be avoided by introducing a dependency on states for the mapping from abstract objects to special urelements. \end{remark} › lemma lambda_rel_extensional: assumes "[❙∀F . ⦇F,a⇧^{P}⦈ ❙≡⦇F,b⇧^{P}⦈ in v]" shows "(❙λx. ⦇R,x⇧^{P},a⇧^{P}⦈) = (❙λx . ⦇R,x⇧^{P}, b⇧^{P}⦈)" proof - interpret MetaSolver . obtain F where F_def: "F = makeΠ⇩_{1}(λ u s w . u = νυ a)" by auto have "[⦇F, a⇧^{P}⦈ ❙≡⦇F, b⇧^{P}⦈ in v]" using assms by (rule AllE) moreover have "[⦇F, a⇧^{P}⦈ in v]" unfolding F_def by (simp add: meta_defs meta_aux) ultimately have "[⦇F, b⇧^{P}⦈ in v]" using EquivE by auto hence "νυ a = νυ b" using F_def by (simp add: meta_defs meta_aux) thus ?thesis by (simp add: meta_defs meta_aux) qed end (*<*) end (*>*)