Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Function calculates Gödel number of negated sentence #15

Open
SnO2WMaN opened this issue Dec 20, 2024 · 1 comment
Open

Function calculates Gödel number of negated sentence #15

SnO2WMaN opened this issue Dec 20, 2024 · 1 comment

Comments

@SnO2WMaN
Copy link
Member

問題意識としては FormalizedFormalLogic/Foundation#108 も参照

文 σ に対して ⌜∼σ⌝ = neg ⌜σ⌝ となる関数 neg の構成と，その利用として “x. ¬!𝔅.prov (neg x)”: $\lnot \mathrm{Pr}(\dot{\lnot}(x))$ のような論理式を考えたいのだが，どう定義すればいいのかよくわからなかった．良い案はあるだろうか？
@iehality
Copy link
Member

形式化された否定なら https://github.com/FormalizedFormalLogic/Arithmetization/blob/3d99d24b572f61cb362e8f40f81697343e3562a6/Arithmetization/ISigmaOne/Metamath/Coding.lean#L477 のように定義してあるのでそれを使えばよいと思う．

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@SnO2WMaN @iehality