A simulating halt decider correctly predicts what the behavior of its input would be if this simulated input never had its simulation aborted. It does this by correctly recognizing several non-halting behavior patterns in a finite number of steps of correct simulation. -/- When simulating halt decider H correctly predicts that directly executed D(D) would remain stuck in recursive simulation (run forever) unless H aborts its simulation of D this directly applies to the halting theorem.

We can simply define Gödel 1931 Incompleteness away by redefining the meaning of the standard definition of Incompleteness: A theory T is incomplete if and only if there is some sentence φ such that (T ⊬ φ) and (T ⊬ ¬φ). This definition construes the existence of self-contradictory expressions in a formal system as proof that this formal system is incomplete because self-contradictory expressions are neither provable nor disprovable in this formal system. Since self-contradictory expressions are neither provable nor disprovable (...) only because they are self-contradictory we could define them as unsound instead of defining the formal system as incomplete. (shrink)

A pair of C functions are defined such that D has the halting problem proof's pathological relationship to simulating termination analyzer H. When H correctly determines that D correctly simulated by H must be aborted to prevent its own infinite execution then H is necessarily correct to reject D as specifying non-halting behavior. This exact same reasoning is applied to the Peter Linz Turing machine based halting problem proof. ...

The conventional notion of a formal system is adapted to conform to the sound deductive inference model operating on finite strings. Finite strings stipulated to have the semantic property of Boolean true provide the sound deductive premises. Truth preserving finite string transformation rules provide valid the deductive inference. Conclusions of sound arguments are derived from truth preserving finite string transformations applied to true premises.

The conventional notion of a formal system is adapted to conform to the sound deductive inference model operating on finite strings. Finite strings stipulated to have the semantic value of Boolean true provide the sound deductive premises. Truth preserving finite string transformation rules provide the valid deductive inference. Sound deductive conclusions are the result of these finite string transformation rules.

Could the intersection of [formal proofs of mathematical logic] and [sound deductive inference] specify formal systems having [deductively sound formal proofs of mathematical logic]? All that we have to do to provide [deductively sound formal proofs of mathematical logic] is select the subset of conventional [formal proofs of mathematical logic] having true premises and now we have [deductively sound formal proofs of mathematical logic].

To eliminate incompleteness, undecidability and inconsistency from formal systems we only need to convert the formal proofs to theorem consequences of symbolic logic to conform to the sound deductive inference model. -/- Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) thus unlike the formal proofs of symbolic logic provability cannot diverge from truth.

Minimal Type Theory (MTT) is based on type theory in that it is agnostic about Predicate Logic level and expressly disallows the evaluation of incompatible types. It is called Minimal because it has the fewest possible number of fundamental types, and has all of its syntax expressed entirely as the connections in a directed acyclic graph.

Within the (Haskell Curry) notion of a formal system we complete Tarski's formal correctness: ∀x True(x) ↔ ⊢ x and use this finally formalized notion of Truth to refute his own Undefinability Theorem (based on the Liar Paradox), the Liar Paradox, and the (Panu Raatikainen) essence of the conclusion of the 1931 Incompleteness Theorem.

Hypothesis: WFF(x) can be applied syntactically to the semantics of formalized declarative sentences such that: WFF(x) ↔ (x ↦ True) ∨ (x ↦ False) (see proof sketch below) For clarity we focus on simple propositions without binary logical connectives.

The possibility of employing human enhancement interventions to aid in future space missions has been gaining attention lately. These possibilities have included one of the more controversial kinds of enhancements: biomedical moral enhancement. However, the discussion has thus far remained on a rather abstract level. In this paper we further this conversation by looking more closely at what type of interventions with what sort of effects we should expect when we are talking about biomedical moral enhancements. We suggest that a (...) more grounded way to picture moral enhancement, at least in the near term, is to envision a form of cognitive enhancement that also provides some moral benefits by heightening the enhanced person's capability for acting according to their own subjective moral code. While this concept of moral adherence enhancement also has relevance for the moral enhancement discussion more widely, in this paper we apply it specifically in the context of space missions. We argue that there are weighty reasons to consider making biomedical enhancements of the proposed kind a mandatory feature of early-phase long-distance space travel because these missions are high-stakes in nature and take place in an environment where the enhancement could be seen as conferring important advantages while negating many of the traditional arguments weighed against it. (shrink)

We begin with the hypothetical assumption that Tarski’s 1933 formula ∀ True(x) φ(x) has been defined such that ∀x Tarski:True(x) ↔ Boolean-True. On the basis of this logical premise we formalize the Truth Teller Paradox: "This sentence is true." showing syntactically how self-reference paradox is semantically ungrounded.

In light of recent breakneck pace in machine learning, questions about whether near-future artificial systems might be conscious and possess moral status are increasingly pressing. This paper argues that as matters stand these debates lack any clear criteria for resolution via the science of consciousness. Instead, insofar as they are settled at all, it is likely to be via shifts in public attitudes brought about by the increasingly close relationships between humans and AI users. Section 1 of the paper I (...) briefly lays out the current state of the science of consciousness and its limitations insofar as these pertain to machine consciousness, and claims that there are no obvious consensus frameworks to inform public opinion on AI consciousness. Section 2 examines the rise of conversational chatbots or Social AI, and argues that in many cases, these elicit strong and sincere attributions of consciousness, mentality, and moral status from users, a trend likely to become more widespread. Section 3 presents an inconsistent triad for theories that attempt to link consciousness, behaviour, and moral status, noting that the trends in Social AI systems will likely make the inconsistency of these three premises more pressing. Finally, Section 4 presents some limited suggestions for how consciousness and AI research communities should respond to the gap between expert opinion and folk judgment. (shrink)

Hehner and Stoddart agree that the halting problem has an inconsistent, unsatisfiable specification. Hehner and Macias agree that a key issue with the halting problem is that it requires a: subjective specification(Hehner) / context dependent function(Macias). When a problem has an unsatisfiable specification because this specification is inconsistent then the unsatisfiability of the specification is anchored in its error thus does not actually limit computation.

Within contemporary science, it is common practice to compare data points to the average, i.e., to the statistical mean. Because this practice is so familiar, it might at first appear not to be the sort of thing that requires explanation. But recent research in cognitive science and in the history of science gives us reason to adopt the opposite perspective. Cognitive science research on the ways people ordinarily make sense of the world suggests that, instead of using a purely statistical (...) notion of the average, people tend to use a value-laden notion of the normal. Similarly, historical research on the scientific practices used in other time periods indicates that, prior to the nineteenth century, scientists tended to make use of a notion of the normal that was overtly value-laden. These findings give us reason to rethink certain familiar facts about scientific practice. In particular, they suggest that the fact that scientists so often make use of the statistical average should be seen as a highly surprising fact, the sort of thing that calls out for explanation. (shrink)

I argue that directing is a more fundamental kind of speech act than asserting, in the sense that the conditions under which an act counts as an assertion are sufficient for that act to count as a directive. I show how this follows from a particular way of conceiving intentionalism about speech acts, on which acts of assertion are attempts at changing a common body of information – or conversational common ground – maintained by conversational participants’ practical attitude of acceptance. (...) I suggest that the function of assertion is not to share information, but to signal that we can be relied on to act as though some information is true, and to foster that same reliability in others. (shrink)

This paper examines some of the interactions between holism, contextualism, and externalism, and will argue that an externalist metasemantics that grounds itself in certain plausible assumptions about self- knowledge will also be a contextualist metasemantics, and that such a contextualist metasemantics in turn resolves one of the best known problems externalist theories purportedly have with self-knowledge, namely the problem of how the possibility of various sorts of ‘switching’ cases can appear to undermine the ‘transparency’ of our thoughts (in particular, our (...) ability to tell, with respect to any two occurrent thoughts, whether they exercise the same or different concepts). (shrink)

Attitude verbs like ‘believe’ and ‘want’ exhibit neg-raising: an ascription of the form a doesn’t believe that p tends to convey that a disbelieves—i.e., believes the negation of—p. In ‘Belief is Weak’, Hawthore et al. observe that neg-raising does not occur with verbs like ‘know’ or ‘need’. According to them, an ascription of the form a believes that p is true just in case a is in a belief state that makes p more likely than not, and so—excepting cases of (...) complete indifference—a will either believe p or disbelieve p. I expand and revise this explanation: so-called ‘weak’ attitude verbs are used in ascriptions of an opinion about some subject matter S—a kind of selection from among the elements of S—and these ascriptions are themselves responsive to conversational topics that presuppose that the subject of the ascription has an opinion about S. ‘Strong’ attitude verbs denote more direct relationships between subject and world. (shrink)

In his 2004 article “Hannah Arendt and Jean Baudrillard: Pedagogy in the Consumer Society,” Trevor Norris bemoans the degree to which contemporary education’s focus can increasingly be described as primarily nurturing “consumers in training.” He goes on to add that the consequences of such “mindless” consumerism is that it “erodes democratic life, reduces education to the reproduction of private accumulation, prevents social resistance from expressing itself as anything other than political apathy, and transforms all human relations into commercial transactions of (...) calculated exchange.” This, then, is the challenge of the age: to articulate the sort of education that might prompt our youngsters to imagine a genuine alternative to this consumer madness—a challenge that the authors of this paper attempt to tackle. (shrink)

A simulating halt decider correctly predicts whether or not its correctly simulated input can possibly reach its own final state and halt. It does this by correctly recognizing several non-halting behavior patterns in a finite number of steps of correct simulation. Inputs that do terminate are simply simulated until they complete.

To the extent that William James had an account of ‘meaning,’ it is best captured in his “pragmatic maxim”, but James’s maxim has notoriously been open to many conflicting interpretations. It will be argued here that some of these interpretive difficulties stem from the fact that (1) James seriously understates the differences between his own views and those presented by Peirce in “How to Make our Ideas Clear”, and (2) James’s understanding of the maxim typically ties meaning to truth, but (...) since James takes “truth” talk to stretch from “temporary” to “absolute” truth, a similar ‘elasticity’ can be found in his conception of meaning. However, this ‘elasticity’ is found in our everyday talk of meaning as well, and James manages to capture it in a more cohesive way than more contemporary accounts that often try to do so by positing two completely distinct types of meaning or content. (shrink)

The novel concept of a simulating halt decider enables halt decider H to to correctly determine the halt status of the conventional “impossible” input D that does the opposite of whatever H decides. This works equally well for Turing machines and “C” functions. The algorithm is demonstrated using “C” functions because all of the details can be shown at this high level of abstraction.

The halting theorem counter-examples present infinitely nested simulation (non-halting) behavior to every simulating halt decider. The pathological self-reference of the conventional halting problem proof counter-examples is overcome. The halt status of these examples is correctly determined. A simulating halt decider remains in pure simulation mode until after it determines that its input will never reach its final state. This eliminates the conventional feedback loop where the behavior of the halt decider effects the behavior of its input.

MIT Professor Michael Sipser has agreed that the following verbatim paragraph is correct (he has not agreed to anything else in this paper) -------> -/- If simulating halt decider H correctly simulates its input D until H correctly determines that its simulated D would never stop running unless aborted then H can abort its simulation of D and correctly report that D specifies a non-halting sequence of configurations.

The novel concept of a simulating halt decider enables halt decider H to to correctly determine the halt status of the conventional “impossible” input D that does the opposite of whatever H decides. This works equally well for Turing machines and “C” functions. The algorithm is demonstrated using “C” functions because all of the details can be shown at this high level of abstraction. ---------------------------------------------------------------------------------------------------- ---- Simulating halt decider H correctly determines that D correctly simulated by H would remain stuck in (...) recursive simulation never reaching its own final state. D cannot do the opposite of the return value from H because this return value is unreachable by every correctly simulated D. This same result is shown to be derived in the Peter Linz Turing machine based proof. (shrink)

This article identifies a novel challenge to standard understandings of responsibility practices, animated by experimental studies of biases and heuristics. It goes on to argue that this challenge illustrates a general methodological challenge for theorizing about responsibility. That is, it is difficult for a theory to give us both guidance in real world contexts and an account of the metaphysical and normative foundations of responsibility without treating wide swaths of ordinary practice as defective. The general upshot is that theories must (...) either hew more closely to actual practice than they appear to, or they must provide some normative foundation for responsibility that does not go through actual practice. (shrink)

In our day-to-day lives, we form responsibility judgements about one another – but we are imperfect beings, and our judgments can be mistaken. This paper suggests that we get things wrong not merely by chance, but predictably and systematically. In particular, these miscues are common when we are dealing with large gaps in social status and power. That is, when we form judgements about those who are much more or less socially powerful than ourselves, it is increasingly likely that “epistemic (...) distorters” will reliably disrupt our reasoning. In response to this situation, I argue for the introduction of a new norm concerning blame and social status: “Powerful Restraint.” This norm suggests that the socially powerful ought to blame the socially dispossessed less frequently, and that social pressure be applied to achieve that compliance. I argue that such a norm is justified given the pernicious down-stream moral effects of the up-stream epistemic distortion I describe. I defend it against objections that it suggests a normative solution to an epistemic problem, that it is paternalistic, and that it involves a kind of disrespect to the less socially powerful. (shrink)

This is an explanation of a possible new insight into the halting problem provided in the language of software engineering. Technical computer science terms are explained using software engineering terms. No knowledge of the halting problem is required. -/- It is based on fully operational software executed in the x86utm operating system. The x86utm operating system (based on an excellent open source x86 emulator) was created to study the details of the halting problem proof counter-examples at the much higher level (...) of abstraction of C/x86. (shrink)

The halting theorem counter-examples present infinitely nested simulation (non-halting) behavior to every simulating halt decider. Whenever the pure simulation of the input to simulating halt decider H(x,y) never stops running unless H aborts its simulation H correctly aborts this simulation and returns 0 for not halting.

By making a slight refinement to the halt status criterion measure that remains consistent with the original a halt decider may be defined that correctly determines the halt status of the conventional halting problem proof counter-examples. This refinement overcomes the pathological self-reference issue that previously prevented halting decidability.

Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to true conclusions without any need for other representations such as model theory.

If the conclusion of the Tarski Undefinability Theorem was that some artificially constrained limited notions of a formal system necessarily have undecidable sentences, then Tarski made no mistake within his assumptions. When we expand the scope of his investigation to other notions of formal systems we reach an entirely different conclusion showing that Tarski's assumptions were wrong.

If there truly is a proof that shows that no universal halt decider exists on the basis that certain tuples: (H, Wm, W) are undecidable, then this very same proof (implemented as a Turing machine) could be used by H to reject some of its inputs. When-so-ever the hypothetical halt decider cannot derive a formal proof from its input strings and initial state to final states corresponding the mathematical logic functions of Halts(Wm, W) or Loops(Wm, W), halting undecidability has been (...) decided. (shrink)

This sentence G ↔ ¬(F ⊢ G) and its negation G ↔ ~(F ⊢ ¬G) are shown to meet the conventional definition of incompleteness: Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)). They meet conventional definition of incompleteness because neither the sentence nor its negation is provable in F (or any other formal system). -- .

This is an explanation of a key new insight into the halting problem provided in the language of software engineering. Technical computer science terms are explained using software engineering terms. -/- To fully understand this paper a software engineer must be an expert in the C programming language, the x86 programming language, exactly how C translates into x86 and what an x86 process emulator is. No knowledge of the halting problem is required.

For any natural (human) or formal (mathematical) language L we know that an expression X of language L is true if and only if there are expressions Γ of language L that connect X to known facts. -/- By extending the notion of a Well Formed Formula to include syntactically formalized rules for rejecting semantically incorrect expressions we recognize and reject expressions that evaluate to neither True nor False.

This paper decomposes the Liar Paradox into its semantic atoms using Meaning Postulates (1952) provided by Rudolf Carnap. Formalizing truth values of propositions as Boolean properties of these propositions is a key new insight. This new insight divides the translation of a declarative sentence into its equivalent mathematical proposition into three separate steps. When each of these steps are separately examined the logical error of the Liar Paradox is unequivocally shown.

Henri Lefebvre has considerable claims to be the greatest living philosopher. His work spans some sixty years and includes original work on a diverse range of subjects, from dialectical materialism to architecture, urbanism and the experience of everyday life. The Production of Space is his major philosophical work and its translation has been long awaited by scholars in many different fields. The book is a search for a reconciliation between mental space and real space. In the course of his exploration, (...) Henri Lefebvre moves from metaphysical and ideological considerations of the meaning of space to its experience in the everyday life of home and city. He seeks, in other words, to bridge the gap between the realms of theory and practice, between the mental and the social, and between philosophy and reality. In doing so, he ranges through art, literature, architecture and economics, and further provides a powerful antidote to the sterile and obfuscatory methods and theories characteristic of much recent continental philosophy. This is a work of great vision and incisiveness. It is also characterized by its author's wit and by anecdote, as well as by a deftness of style which Donald Nicholson-Smith's sensitive translation precisely captures. (shrink)

Tarski "proved" that there cannot possibly be any correct formalization of the notion of truth entirely on the basis of an insufficiently expressive formal system that was incapable of recognizing and rejecting semantically incorrect expressions of language. -/- The only thing required to eliminate incompleteness, undecidability and inconsistency from formal systems is transforming the formal proofs of symbolic logic to use the sound deductive inference model.

A Simulating Halt Decider (SHD) computes the mapping from its input to its own accept or reject state based on whether or not the input simulated by a UTM would reach its final state in a finite number of simulated steps. -/- A halt decider (because it is a decider) must report on the behavior specified by its finite string input. This is its actual behavior when it is simulated by the UTM contained within its simulating halt decider while this (...) SHD remains in UTM mode. (shrink)

Both Tarski and Gödel “prove” that provability can diverge from Truth. When we boil their claim down to its simplest possible essence it is really claiming that valid inference from true premises might not always derive a true consequence. This is obviously impossible.

When we understand that every potential halt decider must derive a formal mathematical proof from its inputs to its final states previously undiscovered semantic details emerge. -/- When-so-ever the potential halt decider cannot derive a formal proof from its input strings to its final states of Halts or Loops, undecidability has been decided. -/- The formal proof involves tracing the sequence of state transitions of the input TMD as syntactic logical consequence inference steps in the formal language of Turing Machine (...) Descriptions. (shrink)

By extending the notion of a Well Formed Formula to include syntactically formalized rules for rejecting semantically incorrect expressions we recognize and reject expressions that have the semantic error of Pathological self-reference(Olcott 2004). The foundation of this system requires the notion of a BaseFact that anchors the semantic notions of True and False. When-so-ever a formal proof from BaseFacts of language L to a closed WFF X or ~X of language L does not exist X is decided to be (...) semantically incorrect. (shrink)

This is the formal YACC BNF specification for Minimal Type Theory (MTT). MTT was created by augmenting the syntax of First Order Logic (FOL) to specify Higher Order Logic (HOL) expressions using FOL syntax. Syntax is provided to enable quantifiers to specify type. FOL is a subset of MTT. The ASSIGN_ALIAS operator := enables FOL expressions to be chained together to form HOL expressions.

An abstract machine having a tape head that can be advanced in 0 to 0x7FFFFFFF increments an unlimited number of times specifies a model of computation that has access to unlimited memory. The technical name for memory addressing based on displacement from the current memory address is relative addressing.

Minimal Type Theory (MTT) shows exactly how all of the constituent parts of an expression relate to each other (in 2D space) when this expression is formalized using a directed acyclic graph (DAG). This provides substantially greater expressiveness than the 1D space of FOPL syntax. -/- The increase in expressiveness over other formal systems of logic shows the Pathological Self-Reference Error of expressions previously considered to be sentences of formal systems. MTT shows that these expressions were never truth bearers, thus (...) never sentences of any formal logic system. (shrink)

When we look at 800,000 year ice core data CO2 levels since 1950 have risen at a rate of 123-fold faster than the fastest rate in 800,000 years. When we see that this rise is precisely correlated with global carbon emissions the human link to climate change seems certain and any rebuttal becomes ridiculously implausible. The 800,000 year correlation between CO2 and global temperatures seems to be predicting at least 9 degrees C of more warming based on current CO2 levels.

This paper presents an overview of the risks and benefits of Social AI, understood as conversational AI systems that cater to human social needs like romance, companionship, or entertainment. Section 1 of the paper provides a brief history of conversational AI systems and introduces conceptual distinctions to help distinguish varieties of Social AI and pathways to their deployment. Section 2 of the paper adds further context via a brief discussion of anthropomorphism and its relevance to assessment of human-chatbot relationships. Section (...) 3 of the paper provides a survey of potential and in some cases demonstrated harms associated with user interactions with Social AI systems. Finally, Section 4 discusses how the benefits and harms of Social AI can best be addressed, with a primary focus on how frameworks from AI ethics can inform their development. (shrink)

Because formal systems of symbolic logic inherently express and represent the deductive inference model formal proofs to theorem consequences can be understood to represent sound deductive inference to deductive conclusions without any need for other representations.

The fail-safe makes sure the fee is high enough to meet carbon emission reduction targets. The safeguard keeps the fee from getting any higher than needed. -/- One of the ways that we could account for the unpredictability of the price elasticity of demand for carbon would be to provide a fail-safe mechanism to ensure that we definitely stay on the carbon reduction schedule. If we keep Energy Innovation Act (HR 763) essentially as it is and scale up the annual (...) carbon fee increase by Number-of-Years-Behind-Schedule * 0.15. (shrink)