This paper presents a formalization of the classical proof of completeness in Henkin-style developed by Troelstra and van Dalen for intuitionistic logic with respect to Kripke models. The completeness proof incorporates their insights in a fresh and elegant manner that is better suited for mechanization. We discuss details of our implementation in the Lean theorem prover with emphasis on the prime extension lemma and construction of the canonical model. Our implementation is restricted to a system of intuitionistic propositional logic with (...) implication, conjunction, disjunction, and falsity given in terms of a Hilbert-style axiomatization. As far as we know, our implementation is the first verified Henkin-style proof of completeness for intuitionistic logic following Troelstra and van Dalen's method in the literature. (shrink)

The fast-paced lifestyle resulting from China's rapid economic development has caused more than 500 million sudden cardiac deaths in 2020. Online first-aid education for the public is considered a key potential solution to avoid such incidents and would have great practical value. This study focuses on understanding the impact of past first-aid experience on the intention for online learning of first-aid knowledge and skills from the perspective of individual psychological factors based on the construction level and prosociality theories. More specifically, (...) it tests the mediating roles of psychological distances and prosociality, which reflect psychological status, in the relationship between experience and learning intention along with a series of associated demographic variables. Primary data collected via a survey are analyzed through regression analysis. The results show that first-aid experience has a significant positive impact on online first-aid learning intention. In addition, psychological distances from first-aid events, and prosociality, play mediating roles in the relationship between first-aid experience and learning intention. Thus, this study contributes to understanding first-aid learning intention by revealing the impact of the individual factors of psychological distances and prosociality. (shrink)

Machine learning methods have been used in multifactor stock strategy for years. This paper uses three machine learning methods and linear regression method to find the most appropriate approach. First, a framework is established and 10 style factors and 30 industry factors are chosen. Second, four methods are used to forecast portfolio returns and compared by predicting returns, successful rate, and Sharpe ratio. Finally, this paper draws conclusion. The main findings are as follows: the support vector regression has the most (...) stable successful rate for predicting, while ridge regression and linear regression have the most unstable successful rate with more extreme cases; algorithm of support vector regression fitting higher-degree polynomials in Chinese A-share market is optimized, compared with the traditional linear regression both in terms of stock return and retracement control; the results of support vector regression significantly outperforming the CSI 500 index prove further. (shrink)

The psychological impact of the COVID-19 epidemic on college students is an important topic. With the entry of the post-epidemic era, how universities can better improve students’ psychological resilience in teaching is the research topic of this article. In the form of a questionnaire survey, some entrepreneurial college students investigated the loneliness and psychological resilience of college students after the outbreak of the epidemic and explored the role of self-efficacy in it. The data is collected online through cooperation with an (...) entrepreneurial event, and the participating students are asked for background information such as colleges, grade, and majors. After collecting this information, they answered a series of simplified scale questions about loneliness, self-efficacy, and psychological resilience. In the end, a total of 200 questionnaires from different universities were collected, and the structural equation model was used to explore the role of self-efficacy. The results show that: loneliness has a significant negative effect on Self-efficacy, β = -0.292, p < 0.001; Self-efficacy has a significant positive effect on psychological resilience, β = 0.556, p < 0.0 01; loneliness has a significant negative effect on psychological resilience, β = -0.244, p < 0.01. Self-Efficacy has a significant intermediate effect in loneliness and psychological resilience, with an effective value of -0.111 and p < 0.01. The results show that this exploratory survey finds it important to provide targeted personal self-efficacy improvement activities for college students with a strong sense of loneliness and to combine school and family education organically to help college students form a healthy and upward mentality to better cope with the unknown and troubles caused by the epidemic, which will help improve the psychological resilience of college students in the epidemic. (shrink)

ObjectiveThis study aims to investigate the effectiveness of mindfulness-based cognitive therapy combined with medication therapy in preventing the recurrence of major depressive disorder in convalescent patients.MethodsA total of 130 patients with convalescent MDD were enrolled in this prospective study. Sixty-five patients were assigned to the experimental group and received medication therapy combined with MBCT, and 65 patients were assigned to the control group and treated with medication alone. The recurrence rate and related hormonal changes were compared between the two groups.ResultsAfter (...) 1 year of MBCT intervention, eight patients experienced recurrence in the experimental group, a recurrence rate of 12.31%, and 19 patients experienced recurrence in the control group, a recurrence rate of 29.23%. The Hamilton Depression Rating Scale and the World Health Organization Quality of Life Scale scores in both the experimental and the control groups were significantly improved after treatment. The difference in the HAM-D scores before and after treatment in the experimental group was 16.74 ± 4.54; this was significantly higher than that of the control group. The WHOQOL-BREF scores in the experimental group were significantly improved compared with those of the control group. The differences in the levels of corticotrophin-releasing hormone, adrenocorticotropic hormone, and cortisol before and after treatment in the experimental group and the control group were statistically significant. The difference in CRH before and after treatment in the experimental group was 16.8 ± 7.2, which was higher than that of the control group. The intervention with MBCT had a significant impact on the recurrence of MDD [β = 1.206, P = 0.039, 95% CI = 0.0790–1.229]. The difference in the HAM-D scores also had a significant impact on the recurrence of MDD.ConclusionCompared with medication therapy alone, the use of MBCT combined with medication therapy can effectively prevent the recurrence of MDD in convalescent patients. (shrink)

A surprisingly large number of lottery prizes go unclaimed every year. This leads us to suspect that what people bet on is not only money, but also good mood. We conducted three studies to explain, from an emotional perspective, why people play lottery games. We first conducted two survey studies to assess mood state reported by online (Study 1a) and offline lottery buyers (Study 1b) at different stages of lottery play. The results revealed that participants’ highest mood appeared before knowing (...) whether they had won. In Study 2, we manipulated the means of reward (lottery tickets vs. cash) and compared participants’ mood changes at different stages of a rewards game in the laboratory. We found the following: first, lottery group participants were generally in a better mood; second, 42% of lottery group participants did not come to the laboratory to collect scratch cards; and third, lottery group participants took more time to return to the laboratory to check their tickets than participants in the cash group. In Study 3, we examined whether priming good or bad mood could influence participants’ preferences for cash versus lottery tickets. The results revealed that participants who were primed for poor mood had a higher preference for lottery tickets compared with their good mood counterparts. These findings suggest that what our participants sought in lottery play was not only money, but improved mood. (shrink)

When there is no immediate response after a proposal and normally the silence is longer than 0.2 s, the proposer would take subsequent actions to pursue a preferred response or mobilize at least an articulated one from the recipient. These actions modulate the prior deontic stance embedded in the original proposal into four trends as follows: maintaining the prior deontic stance with a self-repair or by seeking confirmation; making the prior deontic stance more tentative by making a revised other-attentiveness proposal, (...) providing an account, pursuing with a tag question, or requesting with an intimate address term; making the prior deontic stance more decisive by making a further arrangement, closing the local sequence, or providing a candidate unwillingness account ; and canceling the prior deontic stance by doing a counter-like action. Additionally, these trends inherently embody a decisive-to-tentative gradient. This study would penetrate into the phenomena occurring in Mandarin mundane talk with the methodology of Conversation Analysis to uncover the underflow of deontic stance. (shrink)

As the primary value system in Chinese culture for almost 2,000 years, Confucianism has profoundly influenced the mindset of Chinese people. Cultural psychology studies have highlighted that individuals with different cultural backgrounds vary in their preferences for certain personality traits, such as self-construal, and their metacognitive characteristics, such as thinking modes. Compared with Western cultures, Chinese culture shows a preference for the interdependent self and holistic thinking. To investigate the relationship between the relational-interdependent self, holistic thinking, and traditional Chinese values, (...) we surveyed 327 Chinese adults using the Confucian Traditional Values Survey, Holistic Thinking Scale, and Relational-Interdependent Self-Construal Scale. The results show that Confucian values positively influence both holistic thinking and the relational-interdependent self, the latter of which partially mediates the positive relationship between Confucian values and holistic thinking. This study deepens the understanding of the psychological features of Chinese culture. (shrink)

This study examines Nǐ yìsi shì X ‘Your Meaning is X’ as a practice of doing other-initiation in Mandarin conversations, focusing on how it addresses different sources of troubles systematically in informing sequences. It is found that while ‘Nǐ yìsi shì’ signals the speaker’s having trouble with the prior informing turn, ‘X’ is deployed to locate different aspects of the trouble source, being shaped by how an informing emerges in talk-in-interaction. Specifically, when following a volunteered informing, ‘X’ is usually built (...) to clarify specific words or phrases in preceding informing, thereby treating a certain element as underspecified or ambiguous. However, when following a question-solicited informing, ‘X’ is typically constructed to work out what the provided information exactly conveys, indicating the whole informing turn/action is in some way problematic, inappropriate, or inapposite. In both cases, ‘Nǐ yìsi shì X’ serves as an OI, working to target different kinds of the trouble source, and simultaneously proposes a potential solution to it. (shrink)