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 : % -> %
addmod : (%,%,%) -> %
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.
Polynomials. Polynomials don't have any meaning until you specify the