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!

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.

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'.

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.

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
```

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: Dec 07 2023 at 20:16 UTC