[Agda] HO logic

[Liam O'Connor]

A higher order logic is one that supports quantification of any sort. Typically you need some sort of discipline to stop this becoming inconsistent, for example a type system for your terms.

THE Higher Order Logic typically refers specifically to the logic that uses the simply typed lambda calculus as its term language. It’s not a type theory, so the proof objects aren’t terms, but the terms support abstraction and application. It’s typed to stop you writing a term like

Y not = not (Y not)

which leads to inconsistency (fairly directly) via Curry’s paradox.

Agda is based on ML-TT not HOL, but ML-TT is, logically speaking, also higher order, and is a descendant of the family of higher order logics. Nothing you could prove in (constructive) HOL would be unprovable in Agda.

There are proof assistants based on HOL, specifically Isabelle/HOL, HOL4, and HOLLight, and a variety of smaller ones.

--  
Liam

On 17 October 2015 at 4:33:08 am, Sergei Meshveliani (mechvel at botik.ru) wrote:
> Can people, please, explain
> (in simple words):
>  
> what is a high-order logic?
>  
> Consider the example of a program in Agda:
>  
> --------------------------------------------------------------
> open import Relation.Binary using (Transitive; DecTotalOrder)
> open import Data.Nat as Nat using (ℕ; _≤_)
>  
> open DecTotalOrder Nat.decTotalOrder using () renaming (trans to ≤trans)
>  
> Sequence = ℕ → ℕ
>  
> _≤s_ : Sequence → Sequence → Set _
> f ≤s g = ∀ n → f n ≤ g n
>  
> ≤s-trans : Transitive _≤s_
> ≤s-trans {f} {g} {h} f≤g g≤h n = ≤trans (f≤g n) (g≤h n)
> -------------------------------------------------------------
>  
>  
> ≤s-trans is a proof for a formula that ranges over all infinite
> sequences over ℕ. It proves that the relation _≤s_ on these sequences
> is transitive.
>  
> As Agda type-checks this proof, does this mean that Agda supports an
> high-order logic?
>  
> Are there some more advanced requirements necessary for high-order
> logic?
>  
> Thanks,
>  
> ------
> Sergei
>  
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>