introduction-to-begriff-faa759b2-f4bd-4933-92c3-8ed5f649d822

INTRODUCTION TO BEGRIFF

NOTATION

Concepts has capital letters.

A refer to the concepts' content
:- A refer to a judged concept
-. A The negation of the content
:-. A The nagation of the judgement.
:- A -> B A entails B

ALPHABET. The alphabet for Begriff is quite extensive. For this reason we should start with

BEGRIFF := {A,B,C,D}.
A := {A..Z,a..z}
B := {0..9}
C := {or, and, not, implies, iff}
D := { -, :-, .}

INTRODUCTION. Begriff is a German word for "concept". Concepts are propositions that are judged by any intelect. To judge a concept is to affirm or deny it according to its logical form. Frege, the German logician, developed a language to structure this concepts. A concept has a subject and a predicate, and concepts have categories. I'm trying to simplify things, and if some philosophical concepts are wrong or misplaced is for the sake of programmabilty.

Begriff is meant to describe mathematical concepts, but it can be extended (I don't know how yet) to natural language concepts.

CONCEPTS. I'm going to use Begriff's notation to describe the language itself (metalanguage).

concept - (subject -> predicate)

This is the extension of a subject for example:

A. Socrates is a man.

-A = {Socrates is a man}
:- A = {true}
:-. = {false}

I don't know what Socrates is but I'm extending Socrates by the concept of man. This is an synthetic concept.

concept - (predicate -> subject)

B. All bachelors are single

This is an analytic concept, where "singleness" is included in "bacheloriness".

LOGIC. First thing to be modeled is the propositional logic. It is necessary to test the language in real mathematical proofs such as

There are an infinite number of primes
A number is either prime or composite. Let's say that there is a finite number of primes then,
There is this number be n = p_1p_2...p_n. If we take n+1 this number is not divisible by any p_n. Therefore n+1 is prime. Therefore, there is a infinite number of primes.

In Begriff

def p = (prime)
def n = ()
def m = ()

n = (prime, composite) ; the content
:- n = (composite) ;the assertion
n = (2,3,5,...,m)
p = (prime,composite)
p -. divisible(m) ; n+1 is not composite
p == (prime) ; if p equals a prime it stops.

SEQUENCE BLOCK. One of the good mathematical qualities of Begriff is that loops are obtained by recursion. But, before that, let's introduce the sequence block.

def an = () ; defines an empty sequence block.
def cn = (n) ;defines the sucesessor of n.

;counting

:- an = 0 ; defines a sequence as zero
an = (0)'
if an <= 10 : print an
:- cn = an'
cn == an ; cn equal an
ret

BEGRIFF PROOFS EXAMPLES.

; --- Definitions ---
def N = NaturalNumbersSet ; Concept N represents the set of natural numbers {1, 2, 3, ...}
def M = SetM ; Concept M represents the set M
def m = Element ; Represents a generic element m
def n = Element ; Represents a generic element n
def k = Element ; Represents a generic element k
def One = ConstantValue(1) ; Represents the number 1

def elementOf = Relation(element, set) ; Relation: element is in set
def subsetOf = Relation(set1, set2) ; Relation: set1 is a subset of set2
def equalSets = Relation(set1, set2) ; Relation: set1 equals set2
def multiply = Operation(element, element) ; Operation: multiplication

; --- Defining the Properties of Set M (Based on Interpretation) ---
; Assumption/Base Case: 1 is in M
def M_Base = (elementOf(One, M))
:- M_Base ; Judge/Assert that 1 is indeed in M

; Generative Rule: if m is in M and n is in N, then m*n is in M
; We represent 'if A and B then C' as ':- A -> (:- B -> C)' or similar entailment structure
def M_Rule_Premise1 = elementOf(m, M)
def M_Rule_Premise2 = elementOf(n, N)
def M_Rule_Conclusion = elementOf(multiply(m, n), M)
def M_Rule = (:- M_Rule_Premise1 -> (:- M_Rule_Premise2 -> M_Rule_Conclusion))
; This rule defines the generative property of M.

; --- Goal: Show M equals N ---
Goal = equalSets(M, N)
; To prove Goal, we need to prove subsetOf(N, M) AND subsetOf(M, N)

; --- Part 1: Prove N is a subset of M (subsetOf(N, M)) ---
SubGoal1 = subsetOf(N, M)
; Proof Strategy: Show that any element k in N must also be in M.
; This relies on the base case (1 in M) and the rule (m*n in M).

; Consider any k in N
Assume_k_in_N: :- elementOf(k, N)

; Apply M_Rule with m = One and n = k
Instantiate_Rule_Part1: :- M_Base ; We know 1 is in M
Instantiate_Rule_Part2: :- elementOf(k, N) ; From Assume_k_in_N
Instantiate_Rule_Apply: :- M_Rule -> (elementOf(multiply(One, k), M)) ; If rule holds, conclusion follows for m=1, n=k

; Since we judge M_Base and elementOf(k, N) to be true, we can infer the conclusion:
Infer_k_times_1_in_M: :- elementOf(multiply(One, k), M)

; Since multiply(One, k) is k:
Simplify_k_in_M: :- elementOf(k, M)

; Since k was an arbitrary element assumed to be in N, we conclude N is a subset of M
Conclusion1: :- subsetOf(N, M)

; --- Part 2: Prove M is a subset of N (subsetOf(M, N)) ---
SubGoal2 = subsetOf(M, N)
; Proof Strategy: Show any element m formed according to M's rules must be a Natural Number.
; This uses structural induction based on how elements get into M.

; Base Case: The starting element of M is 1.
BaseCase2_Check: :- elementOf(One, N) ; 1 is a natural number. This holds.

; Inductive Step: Assume m is in M and also m is in N. Show that m*n (where n is in N) is also in N.
InductiveHypothesis: :- elementOf(m, M) -> elementOf(m, N)
Assume_m_in_M: :- elementOf(m, M)
Assume_n_in_N: :- elementOf(n, N)

; Apply Inductive Hypothesis
Infer_m_in_N: :- elementOf(m, N) ; From Assume_m_in_M and InductiveHypothesis

; Property of Natural Numbers: N is closed under multiplication
N_Closure_Prop: (:- elementOf(m, N) -> (:- elementOf(n, N) -> elementOf(multiply(m, n), N)))
:- N_Closure_Prop ; Judge this property of N to be true.

; Apply the closure property
Infer_mn_in_N: :- elementOf(multiply(m, n), N) ; From Infer_m_in_N, Assume_n_in_N, and N_Closure_Prop

; Recall how elements are added to M:
Element_mn_in_M: :- elementOf(multiply(m, n), M) ; This is how new elements are formed (from m in M, n in N)

; Conclusion of Step: Any new element (mn) added to M (Element_mn_in_M) is also in N (Infer_mn_in_N).
; Combined with BaseCase2_Check, this implies all elements of M are in N.
Conclusion2: :- subsetOf(M, N)

; --- Final Conclusion: M equals N ---
Combine_Subsets: (:- subsetOf(N, M) -> (:- subsetOf(M, N) -> equalSets(M, N))) ; Definition of Set Equality
:- Combine_Subsets ; Judge the definition of set equality to be true

; Apply final rule using Conclusion1 and Conclusion2
Final_Assertion1: :- Conclusion1 ; Brings :- subsetOf(N, M) into context
Final_Assertion2: :- Conclusion2 ; Brings :- subsetOf(M, N) into context

FinalConclusion: :- equalSets(M, N) ; Inferred from Combine_Subsets, Final_Assertion1, Final_Assertion2