axiom-developer
[Top][All Lists]

## [Axiom-developer] [15-819] Proofs as math objects

 From: Tim Daly Subject: [Axiom-developer] [15-819] Proofs as math objects Date: Thu, 18 Jan 2018 03:57:04 -0500

I'm a computational mathematician (CM) so I'm coming to the logic
area from left field (deep left, out by the fence). Thus my question
might not make sense.

You made the passing comment that proofs are mathematical
objects like numbers.

What I HEARD was... proofs are like Integers. To a CM that means
(a) there are a set of functions that operate on Integers and
(b) Integers are opaque.

For instance, in Axiom, Integers are:

(1) -> )show Integer
Integer is a domain constructor
Abbreviation for Integer is INT
This constructor is exposed in this frame.
Issue )edit bookvol10.3.pamphlet to see algebra source code for INT ------------------------------- Operations --------------------------------
?*? : (%,%) -> %
?*? : (Integer,%) -> %
?*? : (PositiveInteger,%) -> %
?**? : (%,PositiveInteger) -> %
?+? : (%,%) -> %
?-? : (%,%) -> %
-? : % -> %
?<? : (%,%) -> Boolean
?<=? : (%,%) -> Boolean
?=? : (%,%) -> Boolean
?>? : (%,%) -> Boolean
?>=? : (%,%) -> Boolean
D : % -> %
D : (%,NonNegativeInteger) -> %
OMwrite : (%,Boolean) -> String
OMwrite : % -> String
1 : () -> %
0 : () -> %
?^? : (%,PositiveInteger) -> %
abs : % -> %
associates? : (%,%) -> Boolean
base : () -> %
binomial : (%,%) -> %
bit? : (%,%) -> Boolean
coerce : Integer -> %
coerce : % -> %
coerce : Integer -> %
coerce : % -> OutputForm
convert : % -> String
convert : % -> DoubleFloat
convert : % -> Float
convert : % -> Pattern(Integer)
convert : % -> InputForm
convert : % -> Integer
copy : % -> %
dec : % -> %
differentiate : % -> %
even? : % -> Boolean
factor : % -> Factored(%)
factorial : % -> %
gcd : List(%) -> %
gcd : (%,%) -> %
hash : % -> %
hash : % -> SingleInteger
inc : % -> %
..... etc.

But that seems odd to me, in two ways. First, Proofs seem more like
Polynomials. Polynomials don't have any meaning until you specify the
base ring, e.g. Polynomial(Integer) or Polynomial(Fraction(Integer)).
Once you give me the base ring I know what operations I can perform.

Proofs seem to need the set of sequents and the set of hypotheses in
order to be concrete, e.g. Proof(Heyting,LEM). Without specifying these
constraints I have no idea what a "Proof" means computationally. You
might also have to specify further information (ala Lakatos).

Second, Proofs, like Polynomials, have "internal structure". You can ask a
Polynomial for its leading coefficient. Similarly, you could ask a Proof for
one of its goals. You can write tactics that manipulate the internal structure
of a Proof object (like you can manipulate terms in a Polynomial).

But my question is, given a Proof object as a "mathematical object"
what possible operations can be performed on a proof as an "opaque"
object? Does it make sense to "multiply" proofs? Clearly you can "'and"
them together but I don't know how useful that operation would be.
At most, I might have a "refute" operation but nothing else leaps to mind.

Tim, the confused CM.