-
Notifications
You must be signed in to change notification settings - Fork 2
/
logic.txt
167 lines (127 loc) · 7.64 KB
/
logic.txt
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
logic.txt 0.0.4 UTF-8 dh:2022-11-02
----|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
MISER THEORETICAL CONCEPTION
============================
LOGIC FOR MISER TO LOGIC IN MISER
---------------------------------
<https://github.com/orcmid/miser/blob/master/logic.txt>
There are two ways that logical deductions are employed in the Miser Project
* Application of deductive logics in the formulation of Miser levels,
starting with oMiser
* As mechanized deductive arrangements in Miser itself that are applicable
to Miser itself and potentially other systems, at least those having
computational interpretations in Miser.
[SYNOPSIS: TBD]
[CONTENT: TBD]
NOTES AND BIBLIOGRAPHY
* David A. Wheeler recommended Metamath to my attention. This might be
helpful along with understanding of ACL2. <http://us.metamath.org/>.
* There is cross-over between this treatment and confirming the ‹ob› model
of computation and Church-Turing computability in theory.txt,
<https://github.com/orcmid/miser/blob/master/theory.txt>
* Treatment of logic here relies on the view that "Logic's
main concern is with the soundness and unsndness of arguments, and it
attempts to make as precise as possible the conditions under which an
argument--from whatever field of study--is acceptable [Lemon1978:p.1]."
In this respect, the dismissive "that's not logical" is often itself not
logical.
* We rely on denumerability of obs and applicability of structural induction
in the fundamental logical structures considered in the Miser Project. The
definition of structures is contrived to allow the treatment and discussion
of related but distinct mathematical structures and their formulations.
This will continue into distinguishing computational interpretations used
in representation of such structures, one in another.
[ACL2pedia]
Wikipedia. ACL2 article. Current version available on the Internet at
<https://en.wikipedia.org/wiki/ACL2>. There is a natural affinity of
Miser to the ACL[2] treatment of immutable functional computational
interpretations and development of computational logic. For oMiser, this
level does not seem approachable, although an underlying computational
interpretation is, short of an interface level appropriate to use in
theorem proving about Miser programs and other cases of interest. oFrugal
might not be suitable to that task, although perhaps useful in a bootstrap
of some procedural deduction.
[Barwise1977a]
Barwise, John., Keisler, H.J. (eds). Handbook of Mathematical Logic.
Elsevier (Amsterdam: 1977). ISBN 0-444-86388-5 pbk. An extensive work on
which there is superficial reliance for the Miser Project. The Guides are
helpful in choosing where to look further in parts A (Model Theory),
B (Set Theory), C (Recursion Theory), and D (Proof Theory and Constructive
Mathematics).
[Barwise1977b]
Barwise, John. An Introduction to First-Order Logic. Chapter A.1 in
[Barwise 1977a], pp. 5-46. In the use of formal logic here, a similar
notation is employed for the logical connectives although most definitions
and deductions do not make use of explicit quantifiers, being mainly
equational. With that said, "there are good reasons for considering
first-order logic to be the basic language of mathematics (p.7)."
[BoyerMoore1979]
Boyer, Robert S., Moore, J. Strother. A Computational Logic. Academic
Press (New York: 1979). ISBN 0-12-122950-5. Public domain PDF available
on the Internet at <http://www.cs.utexas.edu/users/boyer/acl.pdf>.
[Crossley1972]
Crossley, J.N., Ash, C.J., Brickhill, C.J., Stillwell, J.C., Williams, N.H.
What Is Mathematical Logic? Dover Publications (New York:1990) ISBN-10
0-486-26404-1 pbk. Republication of Oxford University Press (New York:
1972) edition.
[Lemmon1978]
Lemmon, E.J. Beginning Logic. Hacket (Indianapolis: 1978), ISBN
0-915144-50-6 pbk. Version of the 1965 original modestly updated by George
W. D. Berry. "[I]ntended primarily for students who have no previous
knowledge of the subject, [forming] a working basis for more advanced
reading and ... presented in such a way as to be intelligible to the
layman. The nature of logic is examined, with the gradual introduction of
worked examples." The notation employed differs from that used in The
Miser Project, although it is not difficult to translate. Although this
book is not easy to find, there are affordable (under $10) used versions.
The recommendation of this book, out of a large variety of alternatives,
is for its development of logic as being about sound derivation of logical
consequences.
For the Miser Project we are content to go directly to "truth value"
semantics for their direct applicability to considerations of computation.
Lemmon's more-leisurely development before introduction of truth-value
semantics may be helpful in understanding formal logic's roots in natural
language and rational conduct of human affairs.
Recommended in [Crossley1972].
[Metamath2019]
Megill, Norman., Wheeler, David A. Metamath: A Computer Language for
Mathematical Proofs. Lulu Press (Morrisville, NC: 2019-06-06), ISBN
978-0-3597-0223-7, PDF available on the Internet at
<http://us.metamath.org/downloads/metamath.pdf>.
----|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
Copyright 2020, 2022 Dennis E. Hamilton
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
----|----1----|----2----|----3----|----4----|----5----|----6----|----7----|--*
ATTRIBUTION
Hamilton, Dennis E. Logic for Miser to Logic in Miser. Miser Theoretical
Conception text file logic.txt version 0.0.4 dated 2022-11-02, available
on the Internet as a version of
<https://github.com/orcmid/miser/blob/master/theory.txt>
TODO
* Find a more-accessible modern treatment of logic for beginners.
* Check for other sources that are closer to contemporary treatments and
avoid the Principia Mathematica notation.
* Dig deeper into Metamath once I have an oFrugal REPL and can see how to
apply this, perhaps also in conjunction with Chaitin's AIS LISP codes.
* See if Eugenia Chang's "The Joy of Abstraction" is applicable to ways of
viewing how computational as well as other interpretations are handled
here.
* Put my position paper and slides on Logic for CS Undergraduates somewhere
that they can be linked from here. This should be in a docs/ folio,
but perhaps somewhere like nfoTools rather than only here. Think it over.
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
0.0.4 2022-11-02T15:52Z Manage TODOs
0.0.3 2022-04-10T15:55Z Expand notes and references
0.0.2 2020-07-24-09:29 Add [Metamath2019], related notes and TODOs.
0.0.1 2020-07-15-16:11 Start expanding the annotated bibliography and begin
managing TODO items.
0.0.0 2020-07-12-21:41 Create placeholder on the basic idea.
*** end of logic.txt ***