Objectivism Online Forum

Rate this topic

## Recommended Posts

I've been working on an idea I had a while back that Objectivist Epistemology is equivalent to a fragment of Intuitionistic Type Theory.

From the The Stanford Encyclopedia of Philosophy:

Quote

Intuitionistic type theory (also constructive type theory or Martin-Löf type theory) is a formal logical system and philosophical foundation for constructive mathematics. It is a full-scale system which aims to play a similar role for constructive mathematics as Zermelo-Fraenkel Set Theory does for classical mathematics. It is based on the propositions-as-types principle and clarifies the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic. It extends this interpretation to the more general setting of intuitionistic type theory and thus provides a general conception not only of what a constructive proof is, but also of what a constructive mathematical object is. The main idea is that mathematical concepts such as elements, sets and functions are explained in terms of concepts from programming such as data structures, data types and programs.

Quote

Constructive mathematics is distinguished from its traditional counterpart, classical mathematics, by the strict interpretation of the phrase “there exists” as “we can construct”. In order to work constructively, we need to re-interpret not only the existential quantifier but all the logical connectives and quantifiers as instructions on how to construct a proof of the statement involving these logical expressions.

Quote

Intuitionistic logic encompasses the general principles of logical reasoning which have been abstracted by logicians from intuitionistic mathematics, as developed by L. E. J. Brouwer beginning in his  and . Because these principles also hold for Russian recursive mathematics and the constructive analysis of E. Bishop and his followers, intuitionistic logic may be considered the logical basis of constructive mathematics. Although intuitionistic analysis conflicts with classical analysis, intuitionistic Heyting arithmetic is a subsystem of classical Peano arithmetic. It follows that intuitionistic propositional logic is a proper subsystem of classical propositional logic, and pure intuitionistic predicate logic is a proper subsystem of pure classical predicate logic.

Philosophically, intuitionism differs from logicism by treating logic as a part of mathematics rather than as the foundation of mathematics; from finitism by allowing constructive reasoning about uncountable structures (e.g., monotone bar induction on the tree of potentially infinite sequences of natural numbers); and from Platonism by viewing mathematical objects as mental constructs with no independent ideal existence. Hilbert’s formalist program, to justify classical mathematics by reducing it to a formal system whose consistency should be established by finitistic (hence constructive) means, was the most powerful contemporary rival to Brouwer’s developing intuitionism. In his 1912 essay Intuitionism and Formalism Brouwer correctly predicted that any attempt to prove the consistency of complete induction on the natural numbers would lead to a vicious circle.

I am not the fist to notice that the Objectivist account of concepts is somehow linked to programming. Furthermore, through type theory we can go further and link up the Objectivist notion of concepts with logic in a formal, constructive, and algorithmic way. I hope to use type theory to eventually give a detailed account of higher-order concepts and logic consistent with Objectivism.

I will now explain what I've discovered so far.

According to Objectivism, there are things called "entities" which can have "characteristics" or "attributes". The characteristics themselves can take on several different (finitely many) values which we observe through perception. We can represent characteristics as types quite simply in type theory. Imagine that we live in a very simple universe where there are only three possible characteristics called "Char1" "Char2" and "Char3". Each one can further have one of a small number of values unique to that characteristic.

Inductive Char1 : Type :=
| a : Char1
| b : Char1
| c : Char1.

Inductive Char2 : Type :=
| d : Char2
| e : Char2.

Inductive Char3 : Type :=
| f : Char3
| g : Char3
| h : Char3
| i : Char3.

The first definition above says "Char1 : Type" which is read as "Char1 is of type Type" (more accurately, "Char1 is of sort Type", but don't worry about that for now). It further says that "a : Char1", i.e. "the term 'a' is of type 'Char1'". The term "a" represents the value "a" of the characteristic corresponding to the type "Char1". Similarly for the rest.

Now, an entity can be represented as simply a list listing the values of all of its characteristics. However, some entities are not commensurable, i.e., they don't have the same characteristics. To take that into account, we divide entities into several different kinds according to their characteristics.

Inductive Entity : Type :=
| Kind1 : Char1 -> Char2 -> Char3 -> Entity
| Kind2 : Char2 -> Char3 -> Entity
| Kind3 : Char1 -> Entity
| Kind4 : Char2 -> Entity.

The arrow notation above in "Kind1 : Char1 -> Char2 -> Char3 -> Entity" says that in order to produce an Entity of Kind1, we need to list one term of Char1, then on term of Char2, then one term of Char3. Thus, the terms of the type "Entity" all look like the following examples:

Kind1 a d f

Kind2 e g

Kind3 b

...

and so on.

I assume that concepts can only be formed from entities that are fully commensurable, i.e. are all of the same kind. The reason is, though I have not proven it yet, that mixing entities of different kinds within the same concept can lead to inconsistency. Here is an example of a concept:

Inductive C : Entity -> Prop :=
| is_a_C (e : Entity) (y : Char2) (z : Char3) (H : e = Kind1 a y z) : C e.

The symbol "C" is the name of the concept. Its type is "Entity -> Prop", and so a concept is an abstract function which takes entities as inputs and produces propositions (propositions are types in the sort "Prop") as outputs. The propositions that are produced are described by the last part "C e". It says, essentially "e is a C" (for a concrete example, "Socrates (an entity) is a Man (a concept)"). Since "e" must be an entity, then, concretely, the terms of the type C all look like the following examples:

C (Kind1 a d f) -> "The entity 'Kind1 a d f' is a C"

C (Kind2 e g)

C (Kind1 b d f)

...

Since "C (Kind1 a d f)" is also a proposition, and propositions are just types, what are the terms of "C (Kind1 a d f)"? The terms of the type "C (Kind1 a d f)" are the proofs of the proposition "C (Kind1 a d f)". The stuff to the left of the "C e" tells us how to construct the proofs of the proposition "C e". Specifically, it tells us that we need four things. First, an entity e, then a value y of Char2, then a value z of Char3, and finally a proof H of the proposition "e = Kind1 a y z" , that is, a proof that the entity e is identical to the entity (Kind1 a y z), where a is the value of Char1 (i.e., a constant) from before.

The important thing to take away from all this is that a concept contains lots of non-trivial logical as well as computational structure. Let's look at an example of how a concept may be used. To do that, we prove the following theorem:

Theorem : C (Kind1 a d f)

which, in English, says that "The entity of kind1 whose first characteristic has value a, whose second characteristic has value d, and whose third characteristic has value f is a C". We will prove this using a "backwards style proof", one where we start with the conclusion and then work our way backwards to see what we would have to prove before we can prove it. During the course of the proof, we build up a "proof object", i.e., a term of the type C (Kind1 a d f).

Proof:

Our goal is to prove that C (Kind1 a d f). To do that, we refer to the definition of the concept C. It says that the only way to construct a proof of the proposition C (Kind1 a d f), is to use the "is_a_C" constructor. The "is_a_C" constructor says that we first need an e of type Entity. It is already given to us as (Kind1 a d f), so our proof object so far is is "is_a_C (Kind1 a d f)". The next thing we need is a y of type Char2. For this proof, we will use the value "d" as it is the only one that makes sense. Hence, so far we have "is_a_C (Kind1 a d f) d". We now need a z of type Char3. We choose the value "f" for the same reason as before to get "is_a_C (Kind1 a d f) d f". Finally, we need H a proof of the proposition "e = Kind1 a y z". Since e is just (Kind1 a d f), and y is d and z is f (note that if we had chosen different values for y and z we would not be able to complete the proof), this amounts to saying that we need a proof of the proposition "Kind1 a d f = Kind1 a d f". But this is just true by the law of identity. The Coq implementation of the Calculus of Inductive Constructions provides a term of the law of identity as "eq_refl" (reflexive property of equality) . Hence, this is a valid proof of the proposition H. Our completed proof object is now

(is_a_C (Kind1 a d f) d f eq_refl).

There are a few lessons to learn from this proof. First, it tells us how, exactly, a concept refers to entities. It does so by only allowing entities of the form (Kind1 a * *) through its proof procedure. If we had instead been trying to prove that C (Kind1 a e f) we could have simply chosen the value e for y and we would be able to complete the proof. Thus, this would prove that the entity (Kind1 a e f) is also a C, and we can say that the concept C refers to it. If, on the other hand we had been trying to prove that C (Kind1 b d f) there would be no way to complete the proof whatsoever at the final step since we would never be able to prove the contradiction "Kind1 b d f = Kind1 a d f". The same is true of entities like (Kind2 ...) since the proof would fail right at the start. Therefore, the concept C refers to the entities (Kind1 a * *) where the * represent characteristics whose measurements have been omitted.

Second, it tells us that true propositions such as "C (Kind1 a d f)" will have at least one term in them, while false propositions such as "C (Kind1 b d f)" will be empty.

Third, we can think of the constructor "is_a_C" as a program whose execution terminates if the inputs to it correspond to an entity e that C accepts and evidence y, z, and H that can together prove the proposition (C e), and which never terminates otherwise.

We can even prove theorems like "~ C (Kind1 b d f)" just with what we have so far using the type of reasoning above where we showed why C cannot accept the entity (Kind1 b d f), but I won't be doing so formally here as the proof term that Coq provides is ridiculously complicated (though the proof procedure itself is dead simple).

The machinery we have so far can even be extended to differentiation. For example, we can define a sub-concept of C whose values in its third characteric are restricted to the range of values i and h as follows:

Inductive C_diff : Entity -> Prop :=
| is_a_C_diff  (e  : Entity)
(y  : Char2)
(z  : Char3)
(H0 : e = Kind1 a y z)
(H1 : z = h \/ z = i) : C_diff e.

The last part (H1 : z = h \/ z = i) says that, in addition to the stuff we needed before, we also need a proof of the proposition that the value z is equal to either h or i.

Here is a sample theorem:

Theorem : C_diff (Kind1 a d h).

Proof.

Proceeding analogously as before, we construct (is_a_C_diff (Kind1 a d h) d h eq_refl (--something--)). To complete the proof we need to provide a proof of H1. We note that z = h, and therefore, H1 becomes (h = h \/ h = i). In order to prove an "or-statement" in the Calculus of Inductive Constructions we need to make a choice of either proving the left or right disjunct. Here we will choose the left one which we can prove easily by using eq_refl, and definitely not the right one which is a contradiction. So our completed proof object is now (is_a_C_diff (Kind1 a d h) d h eq_refl (or_introl eq_refl)).

##### Share on other sites

EUREKA!

After several cups of coffee and another sleepless night, I now have an example of a second-order concept. Basically, this concept is a concept about first-order concepts. First-order concepts are those that are directly about entities at the perceptual level, such as the concept C above. The second-order concept I've cooked up, called Valid_1_Conc determines whether a given first-order concept is actually valid or not according to known Objectivist Epistemology. Let's take a look at it:

Inductive Valid_1_Conc : (Entity -> Prop) -> Prop :=
| is_valid (F : Entity -> Prop)
(H : exists (e1 : Entity) (e2 : Entity), F e1 /\ F e2 /\
~(e1 = e2) /\
(forall (x x' : Char1) (y y' : Char2) (z z' : Char3),
(e1 = Kind1 x y z /\ e2 = Kind1 x' y' z') ->
(x = x' \/ y = y' \/ z = z'))) : Valid_1_Conc F.

First, note its type declaration, (Entity -> Prop) -> Prop. This concept takes abstract functions (of which valid first-order concept are a sub-type) and outputs propositions about them. Its constructor requires two inputs. First, a term of type Entity -> Prop. Second a proof of the condition H, which, in English, says that "The concept F must

(1) Accept entities e1 and e2

(2) The entities e1 and e2 cannot be equal (that is, there must be at least two distinct entities that the concept refers to)

(3) The two entities must share a value of at least one characteristic in common, (that is, arbitrary collections of entities are not concepts according to Objectivism as it currently stands)."

The beauty of this thing is that by proving propositions such as (Valid_1_Conc C) as we are about to do, we are precisely validating a first order concept. Here is the theorem:

Theorem : Valid_1_Conc C

Proof.

In order to prove Valid_1_Conc C we use the only constructor available, that being is_valid. "is_valid" requires an F of type Entity -> Prop, but that is already given as C.

The next thing we need is a proof of H. To prove an "exists " statement we must actually produce an entity with the required properties. We see that we actually require two such entities. Let e1 = Kind1 a d f and e2 = Kind1 a e f.

Now, we have to prove a total of four propositions

(1) C (Kind1 a d f)

(2) C (Kind1 a e f)

(3) (Kind1 a d f) =/= (Kind1 a e f)

(4) (forall (x x' : Char1) (y y' : Char2) (z z' : Char3), (e1 = Kind1 x y z /\ e2 = Kind1 x' y' z') ->
(x = x' \/ y = y' \/ z = z'))

The proof of (1) is just the theorem in the previous post, so that's taken care of.

The proof of (2) is just the proof of (1) with "e" chosen instead of "f" at the appropriate step.

To prove (3) we assume that (Kind1 a d f) = (Kind1 a e f) and derive a contradiction. We do so by noting that this works only if a = a, d = e, and f = f. Since the second of these is a contradiction, we're done here.

Proving (4) is not as hard as it seems. Let x, x', y, y', z, and z' be any arbitrary values. The statement now reduces to

"if (e1 = Kind1 x y z /\ e2 = Kind1 x' y' z'), then  (x = x' \/ y = y' \/ z = z')"

Note that e1 = Kind1 a d f and e2 = Kind1 a e f from the "exists" steps so that the hypotheses now say

Kind1 x y z = Kind1 a d f and Kind1 x' y' z' = Kind1 a e f

From this we can immediately derive the six equations:

x = a

x' = a

y = d

y' = e

z = f

z' = f

and we only need to prove one of the disjuncts of x = x' \/ y = y' \/ z = z'. We choose the first one (though the third would work just as well and the second would be impossible).

Since x = a = x', it follows that x = x' and the proof is complete.

The automatically generated proof of this theorem is MONSTROUS, but I'll post it for the curious:

(is_valid C
(ex_intro
(fun e1 : Entity =>
exists e2 : Entity,
C e1 /\
C e2 /\
e1 <> e2 /\
(forall (x x' : Char1) (y y' : Char2) (z z' : Char3),
e1 = Kind1 x y z /\ e2 = Kind1 x' y' z' ->
x = x' \/ y = y' \/ z = z')) (Kind1 a d f)
(ex_intro
(fun e2 : Entity =>
C (Kind1 a d f) /\
C e2 /\
Kind1 a d f <> e2 /\
(forall (x x' : Char1) (y y' : Char2) (z z' : Char3),
Kind1 a d f = Kind1 x y z /\ e2 = Kind1 x' y' z' ->
x = x' \/ y = y' \/ z = z')) (Kind1 a e f)
(conj (_is_a_C (Kind1 a d f) d f eq_refl)
(conj (_is_a_C (Kind1 a e f) e f eq_refl)
(conj
(fun H : Kind1 a d f = Kind1 a e f =>
let H0 :=
eq_ind (Kind1 a d f)
(fun e : Entity =>
match e with
| Kind1 _ d _ => True
| Kind1 _ e _ => False
| Kind2 _ _ => False
| Kind3 _ => False
| Kind4 _ => False
end) I (Kind1 a e f) H
:
False in
False_ind False H0)
(fun (x x' : Char1) (y y' : Char2) (z z' : Char3)
(H : Kind1 a d f = Kind1 x y z /\
Kind1 a e f = Kind1 x' y' z') =>
match H with
| conj H0 H1 =>
let H2 :=
match
H0 in (_ = y0)
return
(y0 = Kind1 x y z -> x = x' \/ y = y' \/ z = z')
with
| eq_refl =>
fun H2 : Kind1 a d f = Kind1 x y z =>
(fun H3 : Kind1 a d f = Kind1 x y z =>
let H4 :=
f_equal
(fun e : Entity =>
match e with
| Kind1 _ _ c2 => c2
| Kind2 _ _ => f
| Kind3 _ => f
| Kind4 _ => f
end) H3
:
f = z in
(let H5 :=
f_equal
(fun e : Entity =>
match e with
| Kind1 _ c1 _ => c1
| Kind2 _ _ => d
| Kind3 _ => d
| Kind4 _ => d
end) H3
:
d = y in
(let H6 :=
f_equal
(fun e : Entity =>
match e with
| Kind1 c0 _ _ => c0
| Kind2 _ _ => a
| Kind3 _ => a
| Kind4 _ => a
end) H3
:
a = x in
(fun H7 : a = x =>
let H8 := H7 : a = x in
eq_ind a
(fun c : Char1 =>
d = y ->
f = z -> c = x' \/ y = y' \/ z = z')
(fun H9 : d = y =>
let H10 := H9 : d = y in
eq_ind d
(fun c : Char2 =>
f = z -> a = x' \/ c = y' \/ z = z')
(fun H11 : f = z =>
let H12 := H11 : f = z in
eq_ind f
(fun c : Char3 =>
a = x' \/ d = y' \/ c = z')
(let H13 :=
match
H1 in (_ = y0)
return
(y0 = Kind1 x' y' z' ->
a = x' \/ d = y' \/ f = z')
with
| eq_refl =>
fun
H13 : Kind1 a e f =
Kind1 x' y' z' =>
(fun
H14 : Kind1 a e f =
Kind1 x' y' z' =>
let H15 :=
f_equal
(fun e : Entity =>
match e with
| Kind1 _ _ c2 => c2
| Kind2 _ _ => f
| Kind3 _ => f
| Kind4 _ => f
end) H14
:
f = z' in
(let H16 :=
f_equal
(fun e0 : Entity =>
match e0 with
| Kind1 _ c1 _ => c1
| Kind2 _ _ => e
| Kind3 _ => e
| Kind4 _ => e
end) H14
:
e = y' in
(let H17 :=
f_equal
(fun e : Entity =>
match e with
| Kind1 c0 _ _ => c0
| Kind2 _ _ => a
| Kind3 _ => a
| Kind4 _ => a
end) H14
:
a = x' in
(fun H18 : a = x' =>
let H19 := H18 : a = x'
in
eq_ind a
(fun c : Char1 =>
e = y' ->
f = z' ->
a = c \/
d = y' \/ f = z')
(fun H20 : e = y' =>
let H21 :=
H20 : e = y' in
eq_ind e
(fun c : Char2 =>
f = z' ->
a = a \/
d = c \/ f = z')
(fun H22 : f = z' =>
let H23 :=
H22 : f = z' in
eq_ind f
(fun c : Char3 =>
a = a \/
d = e \/ f = c)
(or_introl
eq_refl) z'
H23) y' H21) x'
H19) H17) H16) H15) H13
end
:
Kind1 x' y' z' = Kind1 x' y' z' ->
a = x' \/ d = y' \/ f = z' in
H13 eq_refl) z H12) y H10) x H8) H6)
H5) H4) H2
end
:
Kind1 x y z = Kind1 x y z ->
x = x' \/ y = y' \/ z = z' in
H2 eq_refl
end)))))))

Edited by SpookyKitty

##### Share on other sites

I think I sort of get the idea, but I'm not experienced enough in math to really say. Your introductory stuff seems good there, and the bits I could follow or a nice way to phrase things from another perspective, a more formal perspective. But I think it's more the way you wrote it that made it hard to follow, because you use abbreviations a lot. I guess it would make sense from a computer science perspective, but that's what made it difficult.

Would this help advance anything in the field of math? Or computer science? Does it parallel or integrate with some other area within math or logic more broadly speaking?

On 12/12/2019 at 2:48 AM, SpookyKitty said:

However, some entities are not commensurable, i.e., they don't have the same characteristics

I don't think you really defined this well enough. My concern here is that all entities are commensurable by at least one characteristic, namely that, to use the terms of constructive mathematics, all entities are constructible. This doesn't strike me as a huge problem, it might even be minor, but it would help clarify the nature of the characteristics you are talking about.

##### Share on other sites

Characteristics are supposed to be anything you can directly perceive. For example color, texture, shape, etc. Their terms are the values of those characteristics like red, rough, round, etc. I Will make a more detailed submission soon.

Edited by SpookyKitty

##### Share on other sites

Sure, that much I already understood. I was referring to the definition of commensurable, not characteristic.

##### Share on other sites

Two characteriatics A and B are commensurable if and only if they are identical as types. For example, Char1 is commensurable with Char1 and nothing else. Color is commensurable with color and nothing else.

##### Share on other sites

Many places that sell paint offer to color match a sample brought into the store. Instead of red, yellow, blue, it identifies the particular pigment(s) as well as the amount(s) required to match it.

Linguistically, it can be handled with color chips that get described in terms of lighter, darker, brighter, complementaries, clashing, etc.

Programmatically, it is an ambitious project. Familiarity with an objective approach would certainly provide an upper hand in managing such an undertaking.

Known epistemological approaches might be able to be automated. When a program encounters something it hasn't been programmed for, how would that get handled?

Thinking "out loud" here, are there places that java scripts could be used to demonstrate the functionality expected via a web app?

##### Share on other sites
2 hours ago, SpookyKitty said:

Two characteriatics A and B are commensurable if and only if

But the part I quoted earlier was saying that some entities are not commensurable. You didn't say that some characteristics are not commensurable. Yes, the characteristics are distinct, with each characteristic having a finite number of possible values. Then we have entities, which are constructed from a given number of characteristics. We end up with an entity of a specific kind.

My question is, assuming that you are making constructions from reality (rather than seeing what would happen if constructions were made in such a world), can't we say that one of these characteristics we can label "constructible"? We can give it two possible values, 0 and 1. All entities would possess this characteristic; all entities would be constructed with the characteristic "constructible". Some entities are not fully commensurable, I understand that, which is fine. You can't make a concept from every single group of entities. Were you saying that some entities are not even partially commensurable? That's what I was objecting to.

On the other hand, entities are by definition constructible. So we could then ask if instead, characteristics are constructed from entities, in which case you might not even consider "constructible" a characteristic since there is not a possible range of values. There is exactly one value it can hold, because otherwise you couldn't construct it as a characteristic.

Would anything change much if you made it so characteristics are constructed from entities? It might actually make more sense, since at least under Objectivist epistemology, entities are fundamental, and we can't perceptually grasp characteristics until we grasp the entity they stem from.

Edited by Eiuol

##### Share on other sites
10 minutes ago, Eiuol said:

But the part I quoted earlier was saying that some entities are not commensurable. You didn't say that some characteristics are not commensurable. Yes, the characteristics are distinct, with each characteristic having a finite number of possible values. Then we have entities, which are constructed from a given number of characteristics. We end up with an entity of a specific kind.

My question is, assuming that you are making constructions from reality (rather than seeing what would happen if constructions were made in such a world), can't we say that one of these characteristics we can label "constructible"? We can give it to possible values, 0 and 1. All entities would possess this characteristic; all entities would be constructed with the characteristic "constructible". Some entities are not fully commensurable, I understand that, which is fine. You can't make a concept from every single group of entities. Were you saying that some entities are not even partially commensurable? That's what I was objecting to.

Yes, that seems like a very important distinction to keep in mind. The only thing I would change is to avoid naming this characteristic "constructible" and the values "0" and "1", and instead use the terms "hypothetical" and "actual". An entity with the value "hypothetical" denotes an entity that has merely been imagined, whereas the value "actual" denotes an entity that has actually been observed. I'm sure there's a fancy word for this kind of distinction, but I forgot what it was. Is this what you have in mind?

Quote

On the other hand, entities are by definition constructible. So we could then ask if instead, characteristics are constructed from entities, in which case you might not even consider "constructible" a characteristic since there is not a possible range of values. There is exactly one value it can hold, because otherwise you couldn't construct it as a characteristic.

Would anything change much if you made it so characteristics are constructed from entities? It might actually make more sense, since at least under Objectivist epistemology, entities are fundamental, and we can't perceptually grasp characteristics until we grasp the entity they stem from.

Yeah, it would be absurdly hard, since then you would have to reproduce a human-like perceptual system. Instead, the point here is to represent entities as they are represented in conscious reasoning, and, during the course of conscious reasoning, you cannot conceive of a specific entity apart from its characteristics.

## Join the conversation

You can post now and register later. If you have an account, sign in now to post with your account. ×   Pasted as rich text.   Paste as plain text instead

Only 75 emoji are allowed.