Frege's Begriffsschrift

[fl]

I'm reading the formalization of Frege's Begriffsschrift . I'm in favor of formalizing the most famous mathematical

works of the past. Currently there are four of them. Wheeler's works  on scholastic and stoic logics, Frege's Begriffsschrift 

and eventually the Principles of Euclid proposed by myself. In my opinion these works shouldn't be aggregated with the 

rest of set.mm but kept separate in their own sections. They should come with precise references to the original texts. They should be 

conceived as a tool for reading these texts which no longer belong to living mathematics but are a part of its past and 

as such are necessary to understand how we got to where we are. They might be considered as a help to understand texts

that are otherwise difficult to read because of symbols, terms and other features that are outdated. They might be placed after

the official sections in annex ones. 

-- 

FL

[David A. Wheeler]

On Fri, 3 Jul 2020 05:21:38 -0700 (PDT), "'fl' via Metamath" <meta...@googlegroups.com> wrote:
> I'm reading the formalization of Frege's *Begriffsschrift* . I'm in favor

> of formalizing the most famous mathematical
> works of the past.

Sounds good! I love mathematical history, and it's definitely true
that older works can be hard to understand. Principia Mathematica's
notation still gives me a headache, and that's in the recent past, that's barely
over 100 years ago.

> In my opinion
> these works shouldn't be aggregated with the
> rest of set.mm but kept separate in their own sections.

I think we should *not* have such a rigid rule, at least in the sense
that we should definitely allow famous axioms & results in the main body:

- A lot of current mathematics builds on past works. It'd be impossible to *only
have such works later.
- Specific old expressions turn out to have surprising utility;
stoic3 is now used in 71 theorems.
- There are multiple possible goals. I proved
(just) the Stoic indemonstrables and Aristotelian syllogisms early,
but for different reasons.
Proving them early is a good way to demonstrate that the axioms
used in set.mm are at least as strong as those used by
these other works. I think demonstrating that early is important, and
they don't take a lot of space because I made no attempt to prove "everything"
from older works.

> They might be placed after
> the official sections in annex ones.

I think that would make more sense. These sections could formalize older works,
and include comments where certain results are already proven
in the main body.

One challenge is that you will often NOT be able to precisely record exactly the
meanings of the older/other works in a simple way in set.mm, because
their axiom systems & logic are NOT identical to set.mm.
For example, to (mis)use modern terminology, Aristotelian logic only
permits non-empty sets; a common solution (which I applied) is to require
"there exists" in just the specific cases it requires.
That may be okay, because that provides a springboard for comparing our
(more modern) system with theirs, and in some sense a translation of it.
But if you want to precisely capture their logic, I think that in at least some
cases you'll need to create a new database.

--- David A. Wheeler

[fl]

Kept reading Richard Penner's work on Frege's Begriffsschrift yesterday evening.L I compared it with the original text. 

It is very good. It really helps to read Frege's pamphlet. Especially because he uses two-dimension diagrams

to write down formula. So they are hard to read at first. 

My idea of formalizations very close to the text in order to help reading the original texts seems to be validated. 

I propose that a historical section with this material is made.

-- 

FL

[fl]

Moreover Wheeler's idea of adding non-minimized proofs could be applied systematically in these sections.  

They would then constitute genuine material for the training of a  minimization engine based on artificial intelligence. 

The material would be abundant and well delineated in set.mm so that it could be easily 

identified if it is to be removed or minimized later.

-- 

FL

[fl]

Well "minimized" not "removed". 

-- 

FL

[Richard Penner]

Formalization (ax-frege1 through frege133) has been completed and is on the recent proofs page.

What's new is that I have revised statements to embrace class variables as widely as possible for frege70 and later. Quite often this means there is also a corresponding element hypothesis for each as most of these class variables are required to be sets. Formalizing some of Frege's substitutions led to the introduction of the union. frege109 and frege130 will really test your ability to convert between the two notations. Proving dffrege76 was the most challenging part.

NM has stated (can't find where) that he would prefer not move my Frege sections to the main set.mm. I think his preference was for partition of hereditary and Frege from set.mm if the website supported it. Perhaps he may warm to FL's proposal. I am happy that we got some of the work on transitive closure of relations into the main section. My November notes on Frege were lengthy and complex without the t+ function.

[fl]

> I am happy that we got some of the work on transitive closure of relations into the main section.

If a hisitorical section is allowed, I advise you to keep all your proofs in this section. This is the only way to permit your readers to take benefit of your proofs to read Frege's orignal text.

If a theorem about transitive closure deserves to be added to the main sections it may be duplicated.

I also advise you to make a page of advertising for this work with all the bells and whistles  that make you want to read more: photograph, formatting appealing title, introductory paragraph, 

well-chiosen links.. Something stilish and inspiring.

-- 

FL

[fl]

Attractive no ?

-- 

FL

[Norman Megill]

On Thursday, July 9, 2020 at 4:41:43 PM UTC-4, Richard Penner wrote:

NM has stated (can't find where) that he would prefer not move my Frege sections to the main set.mm.

It was here: https://github.com/metamath/set.mm/pull/1604#issuecomment-618464178

 

I think his preference was for partition of hereditary and Frege from set.mm if the website supported it. Perhaps he may warm to FL's proposal. I am happy that we got some of the work on transitive closure of relations into the main section. My November notes on Frege were lengthy and complex without the t+ function.

My basic objection was that it adds new axioms.  set.mm was originally intended to show the derivation of ZFC theorems from a standard set of axioms, and I still think that should be its main purpose.  Adding alternative axioms can be confusing and is probably not interesting to someone who just wants to get into the basics of set theory.  Yesterday I took out the remaining alternate axioms in the prop/pred calc sections (that really shouldn't have been there) and moved most of them to my mathbox for now.

Your work on Frege is very nice.  I had mentioned the possibility of a separate .mm file and directory for it, but in addition to the work needed to create the auxiliary files, it wouldn't necessarily be as visible as having it in set.mm (for example new proofs would not show up on set.mm's Most Recent Proofs page).

Instead, I have been thinking about putting all alternate axiomatizations at the end of the main part of set.mm (just before the start of mathboxes) in a new section called "Historical and alternate axiomatizations", along the lines of what I think FL had in mind.  This will make it impossible for them to be used accidentally in the main part of set.mm,.  Accidental use in mathboxes could still happen in principle, but "(New usage is discouraged.)" tags would largely prevent that, and anyway it would quickly be discovered whenever mathbox material is moved into the main part.  (We can't add a new section after mathboxes without significant changes to metamath.exe, and anyway I'd rather keep to the simpler idea that mathboxes are at the end of set.mm.)

Norm

[Richard Penner]

Not dead!

Back in July, I mined Frege's original work on triple disjunction and conjunction and just last night got them into a PR.

I looked into SVG to reproduce Frege's original notation for the web, and created a mmfrege.raw.html to give examples comparing both the notation and possible idiomatic translations which use set.mm's wider range of notations. Attached is a zip file with the SVG and metamath-processed output file mmfrege.html and a PDF.

[Norman Megill]

This seems very useful for understanding the Frege notation.  I can add it to the mpeuni directory.  However, the mmfrege.html file should pass http://validator.w3.org, and the main header should be centered like on the other  website pages.  Also, there are a large number of separate svg files; perhaps you can prefix the svg file names with "_frege_" so they can be more easily identified.  Currently we are keeping svg files in the same directory as html files (perhaps not the greatest practice, but it's what the site creation scripts currently expect), so the you would reference "fregenotation/jABinS.svg" as "_frege_jABinS.svg" in the html file.

For referencing mmfrege.html in a set.mm comment, you can use "~ mmfrege.html".  The "mm" prefix identifies it as something other than a set.mm label (labels beginning with "mm" are not allowed by "verify markup").

Norm

[Richard Penner]

I think the header is centered the same as say mmzfcnd.raw.html but the lack of the metamath logo causes a distortion in the space available in which to center the title. The HTML validation was fixed by updating the IMG tags to have ALT descriptions and be more HTML-like. There were some broken table header closing tags, now fixed. The main content table has had its maximum width capped at 90% so that you can see it is centered as well, and the column widths have been adjusted to prevent runaway width allocation in the event of a very wide display. 

The English still needs work as I see at least two commas that have no justification for their existence and I haven't yet tackled the really hard to format Frege notations introduced starting with 69. But the work in progress has been shared on my new fregepack branch https://github.com/arpie-steele/set.mm/tree/fregepack