## Stream: Beginner Questions

### Topic: Can you convert from prop back to bool?

#### Isaac Oscar Gariano (Sep 30 2021 at 03:08):

I am curious, would something like this be admissiable in HOL:

``````axiomatization Proptrue :: ‹prop ⇒ bool›  where
prop_iff_bool [simp]: ‹Trueprop (Proptrue P) ≡ P›
``````

Then you can use meta-propositions in HOL ones, e.g:

``````lemma ‹Proptrue(P ⟹ Q) ⟶ (P ⟶  Q)› by(auto)
``````

Sorry if this is a very dumb idea/question, I'm new to Isabelle!

#### Kevin Kappelmann (Sep 30 2021 at 10:52):

admissible is not the right word in this context since your axiomatisation adds theorems about a new constant that previously were not derivable (since the constant did not exist).

I suppose you are interested in whether this would introduce any inconsistencies. I think it would not but you better ask an expert on the mailing list if you want to be sure (or maybe @Simon Roßkopf knows a simple argument?)

In any case, it does not seem like a good idea to add such a constant. Reasoning in isar using meta level connectives is more convenient than using object level connectives.

#### Isaac Oscar Gariano (Sep 30 2021 at 21:36):

Yes your right, I did mean to say consistent, although now I wonder if this would be provable:

``````lemma LPropTrue:
fixes p :: ‹prop›
obtains b :: ‹bool› where ‹Trueprop b ≡ p›
sorry
``````

I have found that using the Pure/prop connectives is easier for Isar, but then I have to use the HOL versions if I want to parse a prop to HOL-only operators (e.g. I can't write ‹THE y . (P(x) ⟹ Q)›)

I also wonder why the HOL operators need to have a seperate 'bool' type and why they can't just be axiomatised for 'prop'.

#### Isaac Oscar Gariano (Sep 30 2021 at 21:56):

Also, on a related note what got me thinking about Proptrue was me trying to make some syntax sugar, but it keeps wrapping things in Trueprop:

``````syntax "_foo" :: ‹prop ⇒ prop ⇒ prop'› (‹⫿_›)
parse_ast_translation ‹[("_foo", fn _ => fn [body] => body)]›
``````

However `prop ‹⫿P›`, and even `‹(⫿(P :: prop)) :: prop›` reports a type error

``````Operator:  Trueprop :: bool ⇒ prop
Operand:   P :: prop
``````

Using `declare [[syntax_ast_trace]]` the AST is apparently:

`````` ("\<^const>HOL.Trueprop" ("_constrain" ("\<^const>HOL.Trueprop" ("_constrain" P <position>)) "\<^type>prop"))
``````

Interstingly, if I don't use ML and instead do

``````translations "⫿P" ⇀ "P"
``````

It works as expected, but that's not sufficient as I have more complicated desugarings I want to do.

#### Kevin Kappelmann (Sep 30 2021 at 23:02):

Isaac Oscar Gariano said:

Yes your right, I did mean to say consistent, although now I wonder if this would be provable:

``````lemma LPropTrue:
fixes p :: ‹prop›
obtains b :: ‹bool› where ‹Trueprop b ≡ p›
sorry
``````

I have found that using the Pure/prop connectives is easier for Isar, but then I have to use the HOL versions if I want to parse a prop to HOL-only operators (e.g. I can't write ‹THE y . (P(x) ⟹ Q)›)

I also wonder why the HOL operators need to have a seperate 'bool' type and why they can't just be axiomatised for 'prop'.

That lemma is unprovable. The best you can do, given your axiomatisation for `Proptrue`, is this:

``````axiomatization Proptrue :: ‹prop ⇒ bool›  where
prop_iff_bool [simp]: ‹Trueprop (Proptrue (PROP P)) ≡ PROP P›

lemma
fixes p :: ‹prop›
obtains ‹Trueprop True ≡ p› | ‹Trueprop False ≡ p›
proof -
assume
h1 : "Trueprop True ≡ p ⟹ thesis" and
h2 : "Trueprop False ≡ p ⟹ thesis"
have p_eq: "Trueprop (Proptrue p) ≡ p" by simp
have
h1' : "Trueprop True ≡ Trueprop (Proptrue p) ⟹ thesis" and
h2' : "Trueprop False ≡ Trueprop (Proptrue p) ⟹ thesis" by
(subst(asm) p_eq | fact h1 | fact h2)+
show thesis
proof (cases "Proptrue p")
case True
have "Trueprop True ≡ Trueprop (Proptrue p)" by (simp add: True)
then show thesis by (rule h1')
next
case False
hence "Trueprop False ≡ Trueprop (Proptrue p)" by simp
then show thesis by (rule h2')
qed
qed
``````

#### Kevin Kappelmann (Sep 30 2021 at 23:04):

You can, in theory, axiomatise all HOL operators to live in `prop` but then you loose the distinction between meta-level and object level logic. You want to keep you meta logic simple and separate from your object logic

Last updated: Aug 13 2022 at 05:18 UTC