Science Score: 44.0%
This score indicates how likely this project is to be science-related based on various indicators:
-
✓CITATION.cff file
Found CITATION.cff file -
✓codemeta.json file
Found codemeta.json file -
✓.zenodo.json file
Found .zenodo.json file -
○DOI references
-
○Academic publication links
-
○Academic email domains
-
○Institutional organization owner
-
○JOSS paper metadata
-
○Scientific vocabulary similarity
Low similarity (3.2%) to scientific vocabulary
Keywords
lean4
logic
Last synced: 10 months ago
·
JSON representation
·
Repository
Formalization of Mathematical Logic
Basic Info
- Host: GitHub
- Owner: FormalizedFormalLogic
- License: apache-2.0
- Language: Lean
- Default Branch: master
- Homepage: https://formalizedformallogic.github.io/Foundation/
- Size: 6.74 MB
Statistics
- Stars: 154
- Watchers: 8
- Forks: 10
- Open Issues: 49
- Releases: 0
Topics
lean4
logic
Created over 3 years ago
· Last pushed 10 months ago
Metadata Files
Readme
License
Citation
README.md
Foundation
Formalizing mathematical logics in Lean 4.
Summary
Main Result in this repository. More results and details are in Book and Doc.
- Propositional Logic
- Tait-style calculus and completeness
- Completeness for Kripke semantics
- Disjunctive Property of intuitionistic logic
- Rejection Law of Excluded Middle in intuitionistic logic and sublogic relations
- Propositional Logic Zoo
- First-Order Logic and Arithmetics
- Completeness Theorem
- Gdel-Gentzen Translation
- Cut-elimination of first-order sequent calculus (Gentzen's Hauptsatz)
- Arithmetic
- Gdel's First and Second Incompleteness Theorems
- Arithmetic Theory Zoo
- Basic Modal Logic (with modal operators $\Box, \Diamond$)
- Provability Logic
Documents
Zoo
Lines represent subset relations of theories/logics. Solid lines are represent proper subset.
Arithmetic Theory Zoo

Modal Logic Zoo

Propositional Logic Zoo

Financial Supports
Any financial supports would greatly helps us. If you considered, please contact us: palalansouki@gmail.com
Previous Sponsors
Companies and organizations that have supported us in the past.
- Proxima Technology (2024-2025)
Owner
- Name: FormalizedFormalLogic
- Login: FormalizedFormalLogic
- Kind: organization
- Repositories: 2
- Profile: https://github.com/FormalizedFormalLogic
Citation (CITATION.cff)
cff-version: 1.2.0 message: "If you use this software, please cite it as below." title: "Formalized Formal Logic" abstract: A mechanized proof library for mathematical logic. authors: - family-names: "Saito" given-names: "Shogo" - family-names: "Noguchi" given-names: "Mashu" type: software repository-code: "https://github.com/FormalizedFormalLogic/Foundation" license: Apache-2.0 date-released: "2023-01-30"
GitHub Events
Total
- Issues event: 136
- Watch event: 64
- Delete event: 224
- Issue comment event: 148
- Push event: 605
- Pull request review event: 59
- Pull request review comment event: 59
- Pull request event: 438
- Fork event: 4
- Create event: 263
Last Year
- Issues event: 136
- Watch event: 64
- Delete event: 224
- Issue comment event: 148
- Push event: 605
- Pull request review event: 59
- Pull request review comment event: 59
- Pull request event: 438
- Fork event: 4
- Create event: 263
Issues and Pull Requests
Last synced: 10 months ago
All Time
- Total issues: 89
- Total pull requests: 279
- Average time to close issues: about 1 month
- Average time to close pull requests: 3 days
- Total issue authors: 3
- Total pull request authors: 3
- Average comments per issue: 0.2
- Average comments per pull request: 0.42
- Merged pull requests: 204
- Bot issues: 3
- Bot pull requests: 7
Past Year
- Issues: 83
- Pull requests: 258
- Average time to close issues: 19 days
- Average time to close pull requests: 3 days
- Issue authors: 3
- Pull request authors: 3
- Average comments per issue: 0.2
- Average comments per pull request: 0.4
- Merged pull requests: 184
- Bot issues: 3
- Bot pull requests: 7
Top Authors
Issue Authors
- SnO2WMaN (70)
- iehality (16)
- github-actions[bot] (3)
Pull Request Authors
- SnO2WMaN (222)
- iehality (50)
- github-actions[bot] (7)
Top Labels
Issue Labels
Pull Request Labels
auto-update-lean (6)