It does not matter what Boolean is.Univalence wrote: ↑Tue May 14, 2019 4:22 pmWhat's aPeteOlcott wrote: ↑Tue May 14, 2019 4:19 pmI am speaking at the meta-mathematical level. You are not speaking at the meta-mathematical level.

This makes what you are saying off-topic.

Truth is only:

(1) Expressions of language defined to have the semantic value of Boolean True.

(2) Valid deductions based on (1).

"Equality" could be stipulated to mean: {go get me an ice cream sandwich right now}

not even having any Boolean value.

The set of expressions of language defined to have the semantic value of Boolean true specifies

the basis of all inference within a formal system.Boolean, Peter?

Somebody familiar with proof theory/dependent type systems would say that a Boolean is a Type.

Why, look! The developers of Idris agree with me.

https://github.com/idris-lang/Idris-dev ... e/Bool.idr

(1) Some expressions of language are defined to have the semantic value of HibGiblet.

(2) Valid deductive inference is HibGiblet preserving.

(3) Therefore valid deductive inference on the basis of HibGiblet expressions necessarily derives a HibGiblet expression.

Within any formal system defined on the basis of sound deductive inference there are no expressions that are not HibGiblet decidable.